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.