Abstract
This paper describes the methods fro automatically analyzing formal,
state-based requiements 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, th analysis is performed
directly on the model. The method scales up to large scale systems by
decompsing the specification into smaller, analyzable parts and then using
functional composition rules to ensure that verifiable properties hold for
the entire specification. The analysis algorithms and tools have been
validated on a TCAS II, a complex, air-borne, collision avoidance system
required on all commercial aircraft with more than 30 passengers that fly in
US airspace.
