Formal Verification Of Real-time Operating System In Binary Code Level

With the rapid development of the science and technology, people are paying more and more attention to the correctness and the safety of the critical software systems which are based on the real-time operating systems. Therefore,the correctness of the real-time operating system is of vital importance. To ensure the correctness and the safety of the real-time operating system, a new approach is proposed for verifying the real-time system in binary code level. The approach which is proposed in this thesis has been applied in the national key project "Research on reliable analyzing and verification approach for Automotive Electronic System" under "Core electronic components, High-end general chips and Infrastructure software" series projects.In this paper, the theory, methodology and tools are proposed. The contributions of the binary code level real-time operating system verification work are listed as follows:1. Embedded Application Oriented Binary Code Intermediate Language-xBIL. It is proposed on this thesis that Embedded Application Oriented Binary Code Interme-diate Language-xBIL (eXtensive Binary Intermediate Languag). xBIL can be used to present the binary code of multiple hardware platforms in a unified form. xBIL which supports the interrupt mechanism, can be used to describe the interrupt be-haviors of the low level program in the operating system. xBIL can also declare the execution time of the instructions, and evaluate the execution time of the program. The approach presents the operational semantics and the denotational semantics of the xBIL, and the equivalence of the two semantics have been proved.2. Bit vector arithmetic and Decision procedure In this paper, a new bit vector arith-metic and it's decision procedure are proposed for deciding the bit vector formulas of xBIL code.3. The approach of verifying the real-time operating system in binary code level. The approach and methodology of verifying the real-time operating system are intro-duced in this paper. Not only the OS specification verification, but also the interrupt safety properties verification are considered in this paper.4. Integrated tools chain for operating system verification The approach which is pro-posed in this thesis has been applied a kind of integrated automatic verification platform. This platform integrates variety of verification tools, and hosts all the tools as services in the enterprise service bus. Through the service adapter of each verification tools, the service coordinates all the verification tools and performs the verification work automatically and efficiently.The approaches above are applied in the verification work of ORIENTAIS RTOS. The application represents the practicality of these approaches. By improving the37bugs which are found by the methodologies of this paper, ORIENTAIS has been certificated by the OSEK international standard group.