Danmin Chen and Zhiguo Chen
B method, task management, specification, proof obligation,implementation
Operating system is the most important software in all computer systems. Because it plays a significant role as a support for other softwares, the operating system must be secure and reliable. The formal method which has rigorous mathematic semantics can be used to specify and verify a software system and its property; thus the formal method is the key to improve security and reliability of software. The goal of this paper is to present a formal model of task management based on B method while it takes embedded real-time operating system MicroC/OS-II as reference. According to the idea of step-wised of B method, this work refines the abstract specification designed in the previous stage and it obtains an achievable model of task management eventually.
Important Links:
Go Back
