Formal embedded operating system model based on resource-based design framework

  • Kim J
  • Sim J
  • Kim C
 et al. 
  • 6


    Mendeley users who have this article in their library.
  • 3


    Citations of this article.


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.

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document


  • Jin Hyun Kim

  • Jae Hwan Sim

  • Chang Jin Kim

  • Jin Young Choi

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free