Proving the shalls

Steven P. Miller, Alan C. Tribble, Mats P.E. Heimdahl

Research output: Chapter in Book/Report/Conference proceedingChapter

13 Scopus citations

Abstract

This paper describes an experiment conducted to determine how effectively formal methods could be used to capture and validate the requirements of a typical embedded system. A model of the mode logic of a Flight Guidance System was specified in the RSML-e notation and translated into the NuSMV model checker and the PVS theorem prover. These tools were then used to verify several hundred properties of the RSML-e model. In the process, several errors were discovered and corrected in the original model. This demonstrates that formal requirements models can be written for real problems and that formal analysis tools have matured to the point where they can be used to find errors before implementation. It also points out a clear relationship between requirements stated informally as "shalls", formal properties, and requirements models.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsKeijiro Araki, Stefania Gnesi, Dino Mandrioli
PublisherSpringer Verlag
Pages75-93
Number of pages19
ISBN (Print)9783540408284
DOIs
StatePublished - 2003

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2805
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint Dive into the research topics of 'Proving the shalls'. Together they form a unique fingerprint.

  • Cite this

    Miller, S. P., Tribble, A. C., & Heimdahl, M. P. E. (2003). Proving the shalls. In K. Araki, S. Gnesi, & D. Mandrioli (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 75-93). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2805). Springer Verlag. https://doi.org/10.1007/978-3-540-45236-2_6