TitleAutomated Consistency Checking of Requirements Specifications
Publication TypeJournal Article
Year of Publication1996
AuthorsHeitmeyer, C. L., R. Jeffords, and B. Labaw
JournalACM Transactions on Software Engineering and Methodology
Volume5
Issue3
Pagination231-261
Abstract

This paper describes a formal analysis technique, called consistency checking, for automatic detection of errors, such as type errors, nondeterminism, missing cases, and circular definitions, in requirements specifications. The technique is designed to analyze requirements specifications expressed in the SCR (Software Cost Reduction) tabular notation. As background, the SCR approach to specifying requirements is reviewed. To provide a formal semantics for the SCR notation and a foundation for consistency checking, a formal requirements model is introduced; the model represents a software system as a finite state automaton, which produces externally visible outputs in response to changes in monitored environmental quantities. Results are presented of two experiments which evaluated the utility and scalability of our technique for consistency checking in a real-world avionics application. The role of consistency checking during the requirements phase of software development is discussed.

Full Text

Heitmeyer etal1996.pdf

NRL Publication Release Number

05-1221-2549