The SCR Requirements Method: Developing High Assurance Software Systems

by Constance Heitmeyer, Naval Research Laboratory

Background

In high assurance systems, compelling evidence is required that the system delivers its services in a manner that satisfies certain critical properties. Examples of high assurance systems include command and control systems, weapons systems, flight programs for commercial and military aircraft, control systems for nuclear plants, and most medical systems (e.g., patient monitoring systems). Critical properties high assurance systems must satisfy including service properties, i.e., properties of the services that the system delivers. For example, when a patient's heart stops, a patient monitoring system may be required to sound an alarm. Besides service properties, four other classes of critical system properties may be identified: security properties, safety properties, real-time properties, and fault-tolerance properties. In most cases, a high assurance system must satisfy properties in more than a single class. The patient monitoring system, for example, must satisfy not only service properties, but real-time constraints (the alarm must sound within some time interval), fault-tolerance properties (the alarm must sound even when a sensor malfunctions), and security properties (the system must protect the privacy of the patient's health records). Note that a given property may fall into more than a single class.

In recent years, researchers have proposed numerous approaches for specifying, constructing, and certifying high assurance systems. These include formal specification notations, formal models, and rigorous verification and validation techniques (such as model checking and mechanical theorem proving). But, two difficult problems remain. The first is the need for technology to support the application of these new techniques and methods to practical systems. Without such technology, opportunities to transfer many of the basic research results to industry are severely limited. Also needed is a unified framework for building systems that satisfy multiple critical properties. This need exists because not one but several different approaches for developing high assurance systems have evolved (at least one for each property class identified above). Each approach has a different overall philosophy of system development and different techniques for specification and assurance. No single one of the separate approaches is sufficient to handle systems now being built that must simultaneously satisfy properties in different classes. Thus a framework (i.e., formal specification techniques, formal models, assurance methods, etc.) is needed for constructing systems that must provide a set of critical services and do so in a secure, safe, timely, and fault-tolerant manner.

The SCR Requirements Method

One framework that has recently been developed for building high assurance control systems is based on the SCR (Software Cost Reduction) requirements method. Originally formulated in 1978 by Naval Research Laboratory (NRL) researchers to document the requirements of the flight program of the Navy's A-7E aircraft⁵, SCR has been used in practice by numerous companies, including Grumann, AT&T, Ontario Hydro, and Lockheed, to specify software requirements. Designed for use by engineers, SCR has been applied to a wide range of systems, including telephone networks, control systems for nuclear plants, and both military and commercial flight control systems.

The SCR method offers a tabular notation for specifying requirements. Underlying this notation is a state machine model. Experience has shown that specifications in the SCR tabular notation are relatively easy for software developers to understand and to construct. Moreover, tables provide a precise, unambiguous basis for communication among developers and a natural organization for independent construction, inspection, modification, and mechanical analysis of parts of a large specification, and finally, the tabular notations scale. Evidence of the scalability of tabular specifications was demonstrated in 1993-94 by engineers at Lockheed, who, in the largest applications of the SCR method to date, used tables to specify the complete requirements of the C-130J flight program, a program containing over 250K lines of Ada code.

The SCR Toolset

Introduced in 1995, SCR^5,6 is an integrated suite of tools supporting the SCR requirements method. It includes a specification editor for creating a requirements specification, a dependency graph browser for displaying the variable dependencies in the specification, a consistency checker for detecting specification errors (e.g., type errors and missing cases), a simulator for validating the specification, and a set of verification tools for checking that the specification satisfies critical application properties, such as security and safety properties. All of the SCR tools are designed for ease of use. Moreover, to the extent feasible, the analyses performed by the tools are fully automatic. Except for the theorem prover (see below), use of the tools requires neither mathematical sophistication nor theorem proving skills. Currently, more than 100 academic, government, and industrial organizations in the US, the UK, Canada, Denmark, and Germany are experimenting with SCR. Further, many universities in both the U.S. and Canada include material on the SCR method and tools in their software engineering courses. The SCR tools are briefly described below.

Specification Editor - To create, modify, or display a requirements specification, the user invokes the specification editor. Each SCR specification is organized into dictionaries and tables. The dictionaries define the static information in the specification, such as the user-defined types and the names and values of variables and constants. Each table specifies how a given variable changes in response to an input event. One important class of tables specifies the values of the system outputs.

Dependency Graph Browser - Understanding the relationship between different parts of a large specification can be difficult. To address this problem, the Dependency Graph Browser (DGB) represents the dependencies among the variables in a given SCR specification as a directed graph. By examining this graph, a user can detect specification errors, e.g., undefined variables and circular definitions. The user can also use the DGB to display, extract, and analyze parts of the dependency graph, e.g., the subgraph containing all variables upon which a given system output depends.

Consistency Checker - The consistency checker³ automatically detects syntax and type errors, variable name discrepancies, missing cases, nondeterminism, and circular definitions. When an error is detected, the consistency checker facilitates error correction by displaying the table (or dictionary) containing the error and highlighting the erroneous entries. It also provides an example that demonstrates the error. A form of static analysis, consistency checking is usually less expensive computationally than model checking. In developing an SCR specification, the user normally invokes the consistency checker first and postpones more expensive analysis, such as model checking, until later. Exploiting the special properties guaranteed by consistency checking (e.g., determinism) can make later analyses more efficient.

Simulator - To validate a specification, the user can run scenarios through the SCR simulator and inspect the results to ensure that the specification captures the intended behavior. Additionally, the user can define properties believed to be true of the required behavior and, using simulation, execute a series of scenarios to determine if any violate the properties. The SCR simulator also supports the construction of graphical front-ends, tailored to particular application domains. One example is a graphical front-end for pilots to use in evaluating an attack aircraft specification (see Figure 1). Rather than clicking on variable names, entering values for them, and seeing the results of simulation presented as variable values, a pilot clicks on visual representations of cockpit controls and views the results on a simulated cockpit display. This front-end allows the pilot to move out of the world of requirements specification and into the world of attack aircraft, where he is the expert. Clearly, a graphical interface facilitates validation of the specification.

Verification Tools. SCR provides three tools for checking that a requirements specification satisfies critical application properties. One tool is the model checker Spin. After a developer uses the SCR tools to generate a tabular representation of the requirements, he can use SCR to automatically translate the tabular representation into the language of Spin. Then, the developer can invoke Spin to check that the specification satisfies properties of interest⁵. If Spin detects a property violation, the developer can then apply the SCR simulator to demonstrate and validate the violation. Because the state space of most specifications of practical systems is usually too large to analyze completely, model checking is typically used to detect violations of properties rather than to verify properties. To verify that an SCR specification satisfies selected properties, the developer may apply either of two additional tools. One tool called TAME¹ (Timed Automata Modeling Environment) is designed to facilitate mechanical theorem proving by reducing the human effort required to prove a property. TAME provides an interface to the mechanical proof system PVS. A second tool called Salsa² uses decision procedures and induction to verify selected properties, in many cases, automatically.

Practical Use of the SCR Tools

To date, the SCR tools have been applied in three pilot projects external to NRL. In the first, researchers at NASA's IV & V Facility used SCR to detect missing cases and instances of nondeterminism in the prose requirements specification of software for the International Space Station. In the second project, engineers at Rockwell Aviation used the tools to expose 24 errors, many of them serious, in the requirements specification of an example flight guidance system. Of the detected errors, a third were uncovered by entering the specification into the toolset, a third in running the consistency checker, and the remaining third in executing the specification with the simulator. In a third project, researchers at the JPL (Jet Propulsion Laboratory) used SCR to analyze specifications of two components of NASA's Deep Space-1 spacecraft for errors.

In addition, NRL has applied SCR to two military systems. In the first, NRL applied the SCR tools to a sizable contractor-produced requirements specification of the Weapons Control Panel (WCP) of a safety-critical weapons system⁵. The tools uncovered numerous errors in the contractor specification, including a safety violation that could result in the malfunction of a weapon. In a second project, NRL used the SCR tools to create and analyze an SCR specification of a moderately complex cryptographic device (CD) for a US Navy radio receiver⁷. Applying the SCR verification tools, demonstrated that the specification satisfies seven security properties but violates an eighth. Especially noteworthy is that, in each project, translating the original specification into the SCR notation, using SCR to analyze the specification for critical properties, and building a simulation (i.e., a working prototype of the system) required slightly more than one person-month. This small effort demonstrates the utility and cost-effectiveness of the SCR method.

Conclusions

The SCR tools can be distinguished in three major ways from commercial tools and other research tools. First, unlike most commercial tools, SCR has a formal foundation, thus allowing mathematically sound analyses (such as consistency checking and model checking), which are unsupported by most current CASE tools. Second, the SCR tools, unlike most research tools, have a well-designed user interface, are integrated to work together, and provide detailed feedback when errors are detected. Finally, users of SCR can perform significant analyses without detailed guidance from application experts or formal methods researchers, thereby providing formal methods usage at low cost.

As demonstrated in the two NRL pilot studies, the SCR method has already been used to specify and to analyze both safety properties and security properties. The method also provides a means of specifying a system's real-time requirements; for example, in the case of the patient monitoring system, the requirement that "an alarm must be sounded within 0.1 seconds after a patient's heart has stopped". Analyzing such requirements specifications to ensure that they satisfy critical real-time properties is a topic of our current research. We are also exploring the use of the SCR method to specify and to analyze a system's fault-tolerance requirements, to construct test cases automatically, and to synthesize efficient source code from validated SCR requirements specifications.

About the Author

Author Contact Information

Constance Heitmeyer heads the Software Engineering Section of the Naval Research Laboratory's Center for High Assurance Computer Systems. Since 1992, her section has been developing a collection of software tools to support the SCR requirements method. In 1996, she and D. Mandrioli published "Formal Methods for Real-Time Computing", a book whose purpose is to introduce practitioners to some of the most promising research results in real-time computing. Also, in 1996, Ms. Heitmeyer served as Program Chair for the COMPASS '96 Conference on Assured Computing. In 1997, she was General Chair of the 1997 International Symposium on Requirements Engineering. She has also served as an Associate Editor of the Real-Time Systems Journal and as a Guest Editor of a special issue of the IEEE Transactions on Software Engineering. Currently, she is a Guest Editor of a special issue of the Kluwer journal, Formal Methods in System Design, which is devoted to tabular expressions in software documentation and analysis. Ms. Heitmeyer frequently teaches tutorials on the SCR approach to software development. Her interests are in requirements specification and analysis, formal methods, and real-time computing and in the transfer of research results into software practice. For a copy of the SCR tools and the User Guide to the tools, send a request to C. Heitmeyer at her E-mail address.

Constance Heitmeyer Naval Research Laboratory (Code 5546) Washington, DC 20375 Phone: (202) 767-3596 Fax: (202) 404-7942 [email protected] www.chacs.itd.nrl.navy.mil/SCR/

---