The Formal Design And Verification Of The Linux 0.11 Schedule Module Based On Isabelle/HOL

With the development of software,people pay more and more attention on the reliability of software,especially for the basic system software like operating system.The Formal methods for operating system design and verification can help achieving higher reliability by strict logic prove.On this basis,it's very necessary to apply the formal method to the operating system.Since most of the operating system is achieved by C language and the kernel of operating system is often in complex form,it's difficult to implement formal verification at the source code level.It's common practice to verify the safety performance of operating system by formal logic verification first and then do the formal analysis on the code.Based on this fact,this paper concerned about the formal method for operating system design and verification and tried to verify part of the system's security characteristics of the formal design.The main work of this paper is shown as follows:Firstly,the kernel code of Linux 0.11 was analyzed and on the basis,the working process from entry of kernel to schedule module was reconstructed and designed by the use of higher order logic language Isabelle/HOL.During the formal design process,one kind of hierarchical design method of PCB was proposed.This method could protect the data in PCB of higher levels and make the operation executed on the data part which can be read concurrently.Also,a kind of extended specification description method was proposed which could not only verify the integrity of kernel system at the abstract level but also verify the scheduling behavior.By this means,the refinement of scheduling behavior could be avoided.Secondly,the condition that the kernel transformation process should meet was defined based on the model construction.Then the reasoning process was conducted by the use of Hoare Logic,Weakest Precondition and rules of theorem prove under the environment of Isabelle.The conclusion demonstrated that the updating and reading process of kernel state was safe and reliable.