COMPLETENESS AND CONSISTENCY IN HIERARCHICAL STATE-BASED REQUIREMENTS

This paper describes methods for automatically analyzing formal, stale -based requirements specifications for some aspects of completeness an d consistency. The approach uses a low-level functional formalism, sim plifying the analysis process. State-space explosion problems are elim inated 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 syst ems by decomposing the specification into smaller, analyzable parts an d then using functional composition rules to ensure that verified prop erties hold for the entire specification. The analysis algorithms and tools have been validated on TCAS II, a complex, airborne, collision-a voidance system required on all commercial aircraft with more than 30 passengers that fly in U.S. airspace.