Abstract
The OSEK/VDX is an international standard of automobile operating systems. Such systems are safety-critical and require extensive safety analysis and verification. Formal methods have been shown useful and effective to verify the safety of both the OSEK/VDX-based operating systems and applications. Using formal methods requires formal semantics of the OSEK/VDX standard. In this paper, we present a formal semantics of the standard using K, a rewrite-based formal semantics framework. With the formal semantics, we can (1) verify user-defined applications by model checking, and (2) automatically generate test cases for testing of the OSEK/VDX-based operating systems. Features of the formal semantics are its executability and flexibility. Compared with existing formal semantics of the standard, the formal semantics defined in K is more flexible and generic. This work also shows that K is not only used for formalizing the semantics of programming languages, but also for automobile operating systems.
| Original language | English |
|---|---|
| Pages (from-to) | 280-296 |
| Number of pages | 17 |
| Journal | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
| Volume | 8663 |
| DOIs | |
| State | Published - 2014 |
Fingerprint
Dive into the research topics of 'A formal semantics of the OSEK/VDX standard in K framework and its applications'. Together they form a unique fingerprint.Cite this
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver