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

Jin Hyun Kim, Jae Hwan Sim, Chang Jin Kim, Jin Young Choi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Citations (Scopus)

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 languageEnglish
Title of host publicationProceedings - International Conference on Quality Software
Pages244-249
Number of pages6
DOIs
Publication statusPublished - 2007 Dec 1
Event7th International Conference on Quality Software, QSIC 2007 - Portland, OR, United States
Duration: 2007 Oct 112007 Oct 12

Other

Other7th International Conference on Quality Software, QSIC 2007
CountryUnited States
CityPortland, OR
Period07/10/1107/10/12

Fingerprint

Hardware
Specifications

ASJC Scopus subject areas

  • Engineering(all)

Cite this

Kim, J. H., Sim, J. H., Kim, C. J., & Choi, J. Y. (2007). Formal embedded operating system model based on resource-based design framework. In Proceedings - International Conference on Quality Software (pp. 244-249). [4385502] https://doi.org/10.1109/QSIC.2007.4385502

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 proceedingConference contribution

Kim, JH, Sim, JH, Kim, CJ & Choi, JY 2007, Formal embedded operating system model based on resource-based design framework. in Proceedings - International Conference on Quality Software., 4385502, pp. 244-249, 7th International Conference on Quality Software, QSIC 2007, Portland, OR, United States, 07/10/11. https://doi.org/10.1109/QSIC.2007.4385502
Kim JH, Sim JH, Kim CJ, Choi JY. Formal embedded operating system model based on resource-based design framework. In Proceedings - International Conference on Quality Software. 2007. p. 244-249. 4385502 https://doi.org/10.1109/QSIC.2007.4385502
Kim, Jin Hyun ; Sim, Jae Hwan ; Kim, Chang Jin ; Choi, Jin Young. / Formal embedded operating system model based on resource-based design framework. Proceedings - International Conference on Quality Software. 2007. pp. 244-249
@inproceedings{959303d1d56e4793be4f79d569669182,
title = "Formal embedded operating system model based on resource-based design framework",
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.",
author = "Kim, {Jin Hyun} and Sim, {Jae Hwan} and Kim, {Chang Jin} and Choi, {Jin Young}",
year = "2007",
month = "12",
day = "1",
doi = "10.1109/QSIC.2007.4385502",
language = "English",
isbn = "0769530354",
pages = "244--249",
booktitle = "Proceedings - International Conference on Quality Software",

}

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 -