Completeness and Consistency in Hierarchical State-Based Requirements

Get BibTex-formatted data

Author

M.P.E. Heimdahl,N.G. Leveson

Entry type

techreport

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.

Address

Seattle, WA 98195

Institution

Michigan State University / University of Wash

Key alpha

Heimdahl

Publication Date

0000-00-00

Location

A hard-copy of this is in the Papers Cabinet

BibTex-formatted data

To refer to this entry, you may select and copy the text below and paste it into your BibTex document. Note that the text may not contain all macros that BibTex supports.

@Techreport{ Heimdahl,
	title = "Completeness and Consistency in Hierarchical State-Based Requirements",
	author = "M.P.E. Heimdahl,N.G. Leveson",
	address = "Seattle, WA 98195",
	institution = "Michigan State University / University of Wash",
	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.",
}