Embedded operating system(OS) is one of most critical software in safety-critical systems. To certify it to a certifi- cation organization, it is recommended that specifications for systems are formally described nowadays. This pa- per 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 so- ciety. 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 mod- els of embedded OS requirement and design separately and verifying them incrementally from functionality and hard- ware's constraints. By means of resource-oriented design, we can identify the property of hardware resources and ac- quire a formally verifiable and executable model of embed- ded OS that can be a proof of its safety.