Completeness and consistency in hierarchical state-based requirements

Mats P.E. Heimdahl, Nancy G. Leveson

Research output: Contribution to journalArticlepeer-review

178 Scopus citations

Abstract

This paper describes methods for automatically analyzing formal, state-based requirements specifications for some aspects of completeness and consistency. The approach uses a low-level functional formalism, simplifying the analysis process. State-space explosion problems are eliminated by applying the analysis at a high level of abstraction; i.e., instead of generating a reachability graph for analysis, the analysis is performed directly on the model. The method scales up to large systems by decomposing the specification into smaller, analyzable parts and then using functional composition rules to ensure that verified properties hold for the entire specification. The analysis algorithms and tools have been validated on TCAS II, a complex, airborne, collision-avoidance system required on all commercial aircraft with more than 30 passengers that fly in U.S. airspace.

Original languageEnglish (US)
Pages (from-to)363-377
Number of pages15
JournalIEEE Transactions on Software Engineering
Volume22
Issue number6
DOIs
StatePublished - 1996

Bibliographical note

Funding Information:
This work has been partially supported by the National Science Foundation Grant CCR-9006279, NASA Grant NAG-1-668, and the National Science Foundation CER Grant DCR-8521398. We would like to thank David Guaspari from Odyssey Research Associates for his feedback on earlier drafts of this paper and his invaluable help with the formal definition of the RSML semantics. David Guaspari was partially supported by the Office of Naval Research, contract number NO01 4-95-5-0349.

Keywords

  • Completeness
  • Consistency
  • Formal methods
  • Formal semantics
  • Reactive systems
  • State-based requirements
  • Static analysis

Fingerprint

Dive into the research topics of 'Completeness and consistency in hierarchical state-based requirements'. Together they form a unique fingerprint.

Cite this