Name
Abstract | ||
|---|---|---|
Automotive systems are widely used in industry and our dailylife. As the reliability of automotive systems is becoming a greater challenge in our community, increasingly more automotive companies are interested in applying formal methods to improve the reliability of automotive systems. We focus on automotive operating systems conforming to the OSEK/VDX standard. Such operating systems are considered as important components to ensure the reliability of the automotive systems. Inprevious work, we proposed a framework to verify the design models of reactive systems against their specifications. This framework allows us to check whether the design model conforms to the specification based on a simulation relation. This paper shows a case study in which the framework is applied to a real design of the OSEK/VDX operating system. As aresult, we found that we were able to check several important properties of the design model. We show the effectiveness and practicality of the framework based on the results of the case study. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1109/TASE.2016.18 | 2016 10th International Symposium on Theoretical Aspects of Software Engineering (TASE) |
Keywords | Field | DocType |
OSEK/VDX OS,formal specification,design model,formal verification,model checking,simulation relation | Model checking,Computer science,OSEK,Real-time computing,Formal specification,Automotive systems,Formal methods,Automotive industry,Formal verification | Conference |
ISBN | Citations | PageRank |
978-1-5090-1765-2 | 1 | 0.35 |
References | Authors | |
8 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Dieu-Huong Vu | 1 | 6 | 1.58 |
| Yuki Chiba | 2 | 35 | 7.46 |
| Kenro Yatake | 3 | 23 | 4.59 |
| Toshiaki Aoki | 4 | 57 | 16.68 |