Formal Embedded Operating System Model Based on Resource-Based Design Framework

Embedded operating system(OS) is one of most critical software in safety-critical systems. To certify it to a certification organization, it is recommended that specifications for systems are formally described nowadays. This paper introduces an executable model of embedded real-time OS of which purpose is to certify an embedded OS, called pCOS, to a certification organization in Korean nuclear society. The behavioral model of embedded OS is built by a design framework, called resource-oriented design. In this framework, we would aim at capturing the behavioral models of embedded OS requirement and design separately and verifying them incrementally from functionality and hardware's constraints. By means of resource-oriented design, we can identify the property of hardware resources and acquire a formally verifiable and executable model of embedded OS that can be a proof of its safety.