Abstract
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.
| Original language | English |
|---|---|
| Title of host publication | Proceedings - International Conference on Quality Software |
| Pages | 244-249 |
| Number of pages | 6 |
| DOIs | |
| Publication status | Published - 2007 Dec 1 |
| Event | 7th International Conference on Quality Software, QSIC 2007 - Portland, OR, United States Duration: 2007 Oct 11 → 2007 Oct 12 |
Other
| Other | 7th International Conference on Quality Software, QSIC 2007 |
|---|---|
| Country | United States |
| City | Portland, OR |
| Period | 07/10/11 → 07/10/12 |
Fingerprint
ASJC Scopus subject areas
- Engineering(all)
Cite this
Formal embedded operating system model based on resource-based design framework. / Kim, Jin Hyun; Sim, Jae Hwan; Kim, Chang Jin; Choi, Jin Young.
Proceedings - International Conference on Quality Software. 2007. p. 244-249 4385502.Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
}
TY - GEN
T1 - Formal embedded operating system model based on resource-based design framework
AU - Kim, Jin Hyun
AU - Sim, Jae Hwan
AU - Kim, Chang Jin
AU - Choi, Jin Young
PY - 2007/12/1
Y1 - 2007/12/1
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=46449093964&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=46449093964&partnerID=8YFLogxK
U2 - 10.1109/QSIC.2007.4385502
DO - 10.1109/QSIC.2007.4385502
M3 - Conference contribution
AN - SCOPUS:46449093964
SN - 0769530354
SN - 9780769530352
SP - 244
EP - 249
BT - Proceedings - International Conference on Quality Software
ER -