Formalization And Verification Of Embedded Operating Systems Using Rewriting Logic

With the development of information science and technology,embedded systems are making progresses more and more rapidly.Embedded systems are often used in various safety-critical areas,such as control systems of aeronautics and astronautics,armariums and automotive electronics.Thus,the soundness and stability of embedded systems are quite important.As the core component of embedded system,its operating system takes responsibility of managing the software and hardware and providing services for users.Therefore,how to guarantee the safety and correctness of the operating system is a key issue on building a trusted embedded system.Thanks to its high degree of mathematics and preciseness,formal methods have been widely used to ensure the reliability of systems.However,due to the limitations of verifiers and the characteristics of operating systems,the application of formal methods to verifying operating systems faces many challenges.For example,the verifiers are not flexible enough to define a general model,which has the capability of analyzing all the components of an operating system.Besides,the operating systems are often implemented in mix language(C and assembly).To unify the system state of C program model and assembler model,some researches abstracted the assembler to C level while some others compile the C program to assembler,which leads to some difficulties on verifying the source program.Based on the challenges faced by the operating system verification,this paper proposes a rewriting-based method to modeling and verifying embedded operating systems.We define semantic models for an automobile operating system specification and kernel respectively.On the basis of the semantic model,we analyze and verify the correctness of operating system specification,kernel and applications respectively.The contributions of this thesis are listed as follows:· We define a complete semantic model for the OSEK operating system specification,which includes all the system services related to task scheduling,resource management,event management,error handling,interrupt mechanism and alarm mechanism.Besides,our semantic model depicts the execution time of system services and system applications.As for the undefined and ambiguous behaviors detected in the specification,we redefine their execution rules and analyze the reliability of our redefinition based on reachability logic proof system.· We propose a method to verifying operating system implementations which are implemented in mixed language.We present operational semantics for basic assembly instructions,a subset of C and C inline assembly.The operational semantics defines execution rules for cases about function calls and sharing variables between two programs implemented in different languages.Based on the semantics,we apply reachability logic proof system to verifying the correctness of mixed language programs and achieve automated verification with the help of K.· We verify an industrial OSEK-based operating system and its application automatically.First of all,based on the complete semantic model of OSEK specification,we verify the correctness of task scheduling,resource management,event management and alarm mechanism,which helps us to choose a reliability interpretation for the undefined(ambiguous)behaviors in the OSEK specification,and analyze the system properties.Furthermore,we verify the operating system kernel and its application provided by the i-soft inc..The verification detected some potential vulnerabilities in the application,which indicates the practicability of our method.