The Open Cybernetics & Systemics Journal

2015, 9 : 1125-1129
Published online 2015 September 10. DOI: 10.2174/1874110X01509011125
Publisher ID: TOCSJ-9-1125

A Formal Specification in B of an Operating System

Chen Danmin , Sun Yue and Chen Zhiguo
Institute of Data and Knowledge Engineering, Henan University, Kaifeng, Henan, 475004, P.R China.

ABSTRACT

Operating system (OS), as a significant system software, provides services and security protection to a variety of applications. Thus, the correctness of OS is a core issue of computer systems. To ensure the correctness of operating systems, it is a recognized way to use the rigorous formal methods. In this paper, we apply B method to design a formal model of OS called fmC/OS. The process is split into two phases. At first, software document specifications are formalized into an abstract model and then the abstract model is implemented into the concrete model. The concrete model is the base of translating executable code. Operating System based on B method can strengthen validity and security of the system.

Keywords:

B method, formal design, operating system, specification.