TY - GEN
T1 - Formalizing application programming interfaces of the OSEK/VDX operating system specification
AU - Zhu, Longfei
AU - Zhang, Min
AU - Huang, Yanhong
AU - Shi, Jianqi
AU - Zhu, Huibiao
PY - 2011
Y1 - 2011
N2 - OSEK/VDX Operating System Specification is a standard in automotive industry with a long history. Dozens of mature industrial operating systems are based on this specification and widely applied in the products of major automotive manufacturers. The verification of the operating system products is always a hard nut to crack. In this paper, we propose a formal specification of OSEK/VDX Operating System based on Hoare Logic, which helps us to get rid of the confusion and ambiguities of the informal specification. In this framework, the formalization of all the Application Programming Interfaces are made. As a case study, we link our framework to the formal verification tool VCC. Some errors are detected in a market-upcoming operating system product based on our framework. We conclude that our framework is feasible in verification of operating system.
AB - OSEK/VDX Operating System Specification is a standard in automotive industry with a long history. Dozens of mature industrial operating systems are based on this specification and widely applied in the products of major automotive manufacturers. The verification of the operating system products is always a hard nut to crack. In this paper, we propose a formal specification of OSEK/VDX Operating System based on Hoare Logic, which helps us to get rid of the confusion and ambiguities of the informal specification. In this framework, the formalization of all the Application Programming Interfaces are made. As a case study, we link our framework to the formal verification tool VCC. Some errors are detected in a market-upcoming operating system product based on our framework. We conclude that our framework is feasible in verification of operating system.
UR - https://www.scopus.com/pages/publications/80055114013
U2 - 10.1109/TASE.2011.12
DO - 10.1109/TASE.2011.12
M3 - 会议稿件
AN - SCOPUS:80055114013
SN - 9780769545066
T3 - Proceedings - 5th International Conference on Theoretical Aspects of Software Engineering, TASE 2011
SP - 27
EP - 34
BT - Proceedings - 5th International Conference on Theoretical Aspects of Software Engineering, TASE 2011
T2 - 5th International Conference on Theoretical Aspects of Software Engineering, TASE 2011
Y2 - 29 August 2011 through 31 August 2011
ER -