This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
2012 IEEE 17th International Conference on Engineering of Complex Computer Systems
ORIENTAIS: Formal Verified OSEK/VDX Real-Time Operating System
Paris, France France
July 18-July 20
ISBN: 978-1-4673-2156-3
In this paper, we report on the formal, machine-verified operating system - ORIENTAIS. ORIENTAIS is an OSEK/VDX standard based real-time operating system for automotive applications. About 8000 lines of C and 60 lines of assembler are comprised in the ORIENTAIS. The operating system is of vital importance to embedded systems, especially for some time sensitive and accurate controlling applications just like automotive applications. We prove that the implementation of ORIENTAIS application programming interfaces strictly follow the OSEK/VDX specification which we formalized from natrual language expressed OSEK/VDX specification. Meanwhile, we model the high level interaction behaviors with CSP and verify the properties just like deadlock-free. To guarantee the safety of memory access and bounded response time with interrupt program involved, binary code level verification is developed based on xBIL which is a binary intermediate language we proposed. We introduce a series of techniques and approaches for verifying the ORIENTAIS. Our approach is an efficient work for the verification of ORIENTAIS, with whose help several bugs are detected. Now, ORIENTAIS has been certificated by OSEK certification group and installed on more than 1.38 million cars in China.
Index Terms:
Safety,Binary codes,Abstracts,Standards,Operating systems,Natural languages,System recovery,Verification,OSEK/VDX,Automotive Electronics,Operating System
Citation:
Jianqi Shi, Jifeng He, Huibiao Zhu, Huixing Fang, Yanhong Huang, Xiaoxian Zhang, "ORIENTAIS: Formal Verified OSEK/VDX Real-Time Operating System," iceccs, pp.293-301, 2012 IEEE 17th International Conference on Engineering of Complex Computer Systems, 2012
Usage of this product signifies your acceptance of the Terms of Use.