A Practical Formal Method for
                  Specifying and Analyzing Software Requirements

			     Constance Heitmeyer
                    Center for High Assurance Computer Systems
		        Naval Research Laboratory
		                Washington, DC 

SCR, a tabular method and notation for specifying software
requirements, was originally formulated in 1979 to document the
requirements of the Operational Flight Program (OFP) for the A-7
aircraft.  Since its introduction, the SCR method has been used in the
development of numerous practical applications, including a telephone
switching network, control software for nuclear power plants, and the
OFP of other avionics systems, including Lockheed's C-130J aircraft.
To provide formal underpinnings for the SCR requirements method and to
facilitate analysis of SCR specifications for errors, we have developed
a state-based formal semantics for the SCR notation and a number of
tools, based on the semantics, for analyzing SCR specifications.  The
tools include a consistency checker and a simulator.  Recently, a model
checking capability was added to the SCR tool set.  Since state machine
models of practical systems have enormous state spaces, techniques are
needed to address the state explosion problem and thus to make model
checking feasible.  This talk briefly reviews the state-machine
semantics of SCR and introduces three sound and complete abstraction
methods that have developed for reducing the state space of SCR
models.  It also describes how two of the abstraction methods were used
recently to expose a safety violation in a requirements specification
of a safety-critical military system.

-------------------------------------------------------------------------

Connie Heitmeyer heads the Software Engineering Section of the Naval
Research Laboratory's Center for High Assurance Computer Systems.  In
1996, she was coeditor of a book entitled "Formal Methods for
Real-Time Computing."  Recently, she served as program chair for the
COMPASS '96 Conference on Assured Computing and general chair for the
1997 International Symposium on Requirements Engineering. Her research
is in requirements specification, formal methods, and real-time
computing.