kirancodes.me
To Proof Maintenance & Beyond!
ICSE 1995

Completeness and Consistency Analysis of State-Based Requirements

Mats Per Erik Heimdahl, Nancy G. Leveson

PDFDOI 10.1145/225014.225015dblp

Abstract

This paper describes methods for automatically analyzing formal, state-based requirements specifications for completeness and consistency.The approach uses a low-level functional formalism, simplifying the analysis process.State space exploslon 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 reqmred on all commercial aircraft with more than 30 passengers that fly in U.S. airspace.

BibTeX
@inproceedings{Heimdahl-Leveson:ICSE95,
  author    = {Mats Per Erik Heimdahl and
               Nancy G. Leveson},
  title     = {Completeness and Consistency Analysis of {State-Based} Requirements},
  booktitle = {ICSE},
  pages     = {3--14},
  publisher = {{ACM}},
  year      = {1995},
}

Related papers