TY - JOUR
T1 - A formal semantics of the OSEK/VDX standard in K framework and its applications
AU - Zhang, Min
AU - Choi, Yunja
AU - Ogata, Kazuhiro
N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2014.
PY - 2014
Y1 - 2014
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84911976947&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-12904-4_16
DO - 10.1007/978-3-319-12904-4_16
M3 - Article
AN - SCOPUS:84911976947
SN - 0302-9743
VL - 8663
SP - 280
EP - 296
JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ER -