Completeness and Consistency in Hierarchical State-Based Requirements,

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 1995
Accession Number
ADA327598

Entities

People

  • Mats. P. Heimdahl
  • Nancy Leveson

Organizations

  • Michigan State University

Tags

Communities of Interest

  • Engineered Resilient Systems

DTIC Thesaurus Topics

  • Aircrafts
  • Algorithms
  • Boundaries
  • Collision Avoidance
  • Collision Avoidance Systems
  • Commercial Aircraft
  • Complex Systems
  • Computer Science
  • Consistency
  • Engineering
  • Errors
  • Explosions
  • Hierarchies
  • Language
  • Military Research
  • Models
  • Software Development

Fields of Study

  • Computer science

Readers

  • Adaptive Control and Estimation with Uncertainty in Dynamic Systems.
  • Aviation Safety and Air Traffic Management
  • Software Engineering.

Technology Areas

  • Space