Paris, France France
July 18, 2012 to July 20, 2012
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.
Safety, Binary codes, Abstracts, Standards, Operating systems, Natural languages, System recovery, Verification, OSEK/VDX, Automotive Electronics, Operating System
Jianqi Shi, Jifeng He, Huibiao Zhu, Huixing Fang, Yanhong Huang, Xiaoxian Zhang, "ORIENTAIS: Formal Verified OSEK/VDX Real-Time Operating System", ICECCS, 2012, Engineering of Complex Computer Systems, IEEE International Conference on, Engineering of Complex Computer Systems, IEEE International Conference on 2012, pp. 293-301, doi:10.1109/ICECCS.2012.27