Model checking RSML-e requirements

Yunja Choi, M. P.E. Heimdahl

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

23 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 languageEnglish (US)
Title of host publicationProceedings - 7th IEEE International Symposium on High Assurance Systems Engineering, HASE 2002
PublisherIEEE Computer Society
Pages109-118
Number of pages10
ISBN (Electronic)0769517692
DOIs
StatePublished - Jan 1 2002
Event7th IEEE International Symposium on High Assurance Systems Engineering, HASE 2002 - Tokyo, Japan
Duration: Oct 23 2002Oct 25 2002

Publication series

NameProceedings of IEEE International Symposium on High Assurance Systems Engineering
Volume2002-January
ISSN (Print)1530-2059

Other

Other7th IEEE International Symposium on High Assurance Systems Engineering, HASE 2002
CountryJapan
CityTokyo
Period10/23/0210/25/02

Keywords

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

Fingerprint Dive into the research topics of 'Model checking RSML<sup>-e</sup> requirements'. Together they form a unique fingerprint.

Cite this