Design Of Embedded Real-Time Operating System Based On B Method

With the flourishing applications,the coherence and reliability of computer systems are more and more crucial.Operating System is the most important software in any computer systems,which plays the role as the support and base for all the other systems,so the Operating System must be secure and reliable.However,with the limitations of traditional software development methods,the security and reliability of Operating Systems cannot be very well supported.The formal methods have strict mathematic semantics,which can be used to specify and verify a software system and its property,clearly,accurately,and abstractly. These methods can help developers to find design defects in the early development stages,thus may improve safety and reliability of software greatly.Formal methods have become a kind of important methods to ensure the validity and consistence in the development of the software.B method is one of the most popular formal methods at present,which supports the whole lifecycle of software development process,from specification to code generation. Taking the precise mathematics semantics as the foundation,B method supports rigorous development process.With the top-down formal specifications and related proofs,the developers may find and get rid of many design and implementation errors in the early development stages,so that the resulting software can be more coherent and reliable.In this paper,we use B method to design a formal model of Operating System called fmC/OS.The fmC/OS is similar toμC/OS-Ⅱthat is a widely used Embedded Real-Time Operating System.The main work described here is as follows:First,we study thought of formal development and basic knowledge of B method including the specification mechanism,process of refinement,generation and proof of proof obligation,composition mechanism,developing process of B method and so on. Second,we take Embedded Real-Time Operating SystemμC/OS-Ⅱas chief reference,and uses B method to design a formal model of Operating System called fmC/OS.Main function units of this Operating System include task management, memory management and inter-task synchronization and communication.By analyzing the system functionality,we divide the Operating System into several sub-systems,the design of all the subsystem models is developed using B method.Proof obligations are generated in this stage,and are proved by B tools.Finally,according to the idea of step-wised construction of B method,we refine the abstract specification models designed in the previous stage,and prove "refinement relationship theorems" which are generated in the refinement stage,thus ensure the consistency of refinement model and original abstract model.This work achieves a realizable model of Operating System eventually.Real-Time Operating System developed based on B method may improve the system validity and security.