Model checking RSML-e requirements

Yunja Choi; M. P.E. Heimdahl

doi:10.1109/HASE.2002.1173111

Model checking RSML^-e requirements

Yunja Choi, M. P.E. Heimdahl

Computer Science and Engineering

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

25 Scopus citations

Abstract

Model checking is a promising technique for automated verification or refutation of software systems. Nevertheless, it has not been used widely in practice mainly due to the lack of the supporting tools that incorporate the model checking activity into the development process. As a part of our overall method supporting specification centered system development, we have implemented a translator between a formal specification language RSML^-e and a symbolic model checker NuSMV. Our translation and abstraction approach aims at usability in practice so that model checking can be used as a routine process during requirement analysis without requiring much knowledge about formal methods. Preliminary results from applying the system in a commercial setting is quite promising. We discuss our translation and abstraction approach in some depth and illustrate its feasibility with some preliminary results.

Original language	English (US)
Title of host publication	Proceedings - 7th IEEE International Symposium on High Assurance Systems Engineering, HASE 2002
Publisher	IEEE Computer Society
Pages	109-118
Number of pages	10
ISBN (Electronic)	0769517692
DOIs	https://doi.org/10.1109/HASE.2002.1173111
State	Published - 2002
Event	7th IEEE International Symposium on High Assurance Systems Engineering, HASE 2002 - Tokyo, Japan Duration: Oct 23 2002 → Oct 25 2002

Publication series

Name	Proceedings of IEEE International Symposium on High Assurance Systems Engineering
Volume	2002-January
ISSN (Print)	1530-2059

Other

Other	7th IEEE International Symposium on High Assurance Systems Engineering, HASE 2002
Country/Territory	Japan
City	Tokyo
Period	10/23/02 → 10/25/02

Bibliographical note

Publisher Copyright:
© 2002 IEEE.

Keywords

Computer science
Electronic mail
Engineering management
Formal specifications
Memory management
Modeling
NASA
Software systems
Specification languages
Usability

Access

10.1109/HASE.2002.1173111

OpenUrl availability

Full text

Cite this

Choi, Y., & Heimdahl, M. P. E. (2002). Model checking RSML^-e requirements. In Proceedings - 7th IEEE International Symposium on High Assurance Systems Engineering, HASE 2002 (pp. 109-118). Article 1173111 (Proceedings of IEEE International Symposium on High Assurance Systems Engineering; Vol. 2002-January). IEEE Computer Society. https://doi.org/10.1109/HASE.2002.1173111

Model checking RSML^-e requirements. / Choi, Yunja; Heimdahl, M. P.E.
Proceedings - 7th IEEE International Symposium on High Assurance Systems Engineering, HASE 2002. IEEE Computer Society, 2002. p. 109-118 1173111 (Proceedings of IEEE International Symposium on High Assurance Systems Engineering; Vol. 2002-January).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Choi, Y & Heimdahl, MPE 2002, Model checking RSML^-e requirements. in Proceedings - 7th IEEE International Symposium on High Assurance Systems Engineering, HASE 2002., 1173111, Proceedings of IEEE International Symposium on High Assurance Systems Engineering, vol. 2002-January, IEEE Computer Society, pp. 109-118, 7th IEEE International Symposium on High Assurance Systems Engineering, HASE 2002, Tokyo, Japan, 10/23/02. https://doi.org/10.1109/HASE.2002.1173111

@inproceedings{e43fdb8c99124377861857edcbb22293,

title = "Model checking RSML-e requirements",

abstract = "Model checking is a promising technique for automated verification or refutation of software systems. Nevertheless, it has not been used widely in practice mainly due to the lack of the supporting tools that incorporate the model checking activity into the development process. As a part of our overall method supporting specification centered system development, we have implemented a translator between a formal specification language RSML-e and a symbolic model checker NuSMV. Our translation and abstraction approach aims at usability in practice so that model checking can be used as a routine process during requirement analysis without requiring much knowledge about formal methods. Preliminary results from applying the system in a commercial setting is quite promising. We discuss our translation and abstraction approach in some depth and illustrate its feasibility with some preliminary results.",

keywords = "Computer science, Electronic mail, Engineering management, Formal specifications, Memory management, Modeling, NASA, Software systems, Specification languages, Usability",

author = "Yunja Choi and Heimdahl, {M. P.E.}",

note = "Publisher Copyright: {\textcopyright} 2002 IEEE.; 7th IEEE International Symposium on High Assurance Systems Engineering, HASE 2002 ; Conference date: 23-10-2002 Through 25-10-2002",

year = "2002",

doi = "10.1109/HASE.2002.1173111",

language = "English (US)",

series = "Proceedings of IEEE International Symposium on High Assurance Systems Engineering",

publisher = "IEEE Computer Society",

pages = "109--118",

booktitle = "Proceedings - 7th IEEE International Symposium on High Assurance Systems Engineering, HASE 2002",

}

TY - GEN

T1 - Model checking RSML-e requirements

AU - Choi, Yunja

AU - Heimdahl, M. P.E.

PY - 2002

Y1 - 2002

N2 - Model checking is a promising technique for automated verification or refutation of software systems. Nevertheless, it has not been used widely in practice mainly due to the lack of the supporting tools that incorporate the model checking activity into the development process. As a part of our overall method supporting specification centered system development, we have implemented a translator between a formal specification language RSML-e and a symbolic model checker NuSMV. Our translation and abstraction approach aims at usability in practice so that model checking can be used as a routine process during requirement analysis without requiring much knowledge about formal methods. Preliminary results from applying the system in a commercial setting is quite promising. We discuss our translation and abstraction approach in some depth and illustrate its feasibility with some preliminary results.

AB - Model checking is a promising technique for automated verification or refutation of software systems. Nevertheless, it has not been used widely in practice mainly due to the lack of the supporting tools that incorporate the model checking activity into the development process. As a part of our overall method supporting specification centered system development, we have implemented a translator between a formal specification language RSML-e and a symbolic model checker NuSMV. Our translation and abstraction approach aims at usability in practice so that model checking can be used as a routine process during requirement analysis without requiring much knowledge about formal methods. Preliminary results from applying the system in a commercial setting is quite promising. We discuss our translation and abstraction approach in some depth and illustrate its feasibility with some preliminary results.

KW - Computer science

KW - Electronic mail

KW - Engineering management

KW - Formal specifications

KW - Memory management

KW - Modeling

KW - NASA

KW - Software systems

KW - Specification languages

KW - Usability

UR - http://www.scopus.com/inward/record.url?scp=84903618392&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84903618392&partnerID=8YFLogxK

U2 - 10.1109/HASE.2002.1173111

DO - 10.1109/HASE.2002.1173111

M3 - Conference contribution

AN - SCOPUS:84903618392

T3 - Proceedings of IEEE International Symposium on High Assurance Systems Engineering

SP - 109

EP - 118

BT - Proceedings - 7th IEEE International Symposium on High Assurance Systems Engineering, HASE 2002

PB - IEEE Computer Society

T2 - 7th IEEE International Symposium on High Assurance Systems Engineering, HASE 2002

Y2 - 23 October 2002 through 25 October 2002

ER -