APPLYING THE B METHOD FOR THE RIGOROUS DEVELOPMENT OF TASK MANAGEMENT

Danmin Chen and Zhiguo Chen

Keywords

B method, task management, specification, proof obligation,implementation

Abstract

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