Tools for Constructing Requirements Specification: The SCR Toolset at the Age of Ten

摘要

While human effort is critical to creating requirements specifications and human inspection can detect many specification errors, software tools find errors inspections miss and also find certain classes of errors more cheaply. This paper describes a set of tools for constructing and analyzing requirements specifications in the SCR (Software Cost Reduction) tabular notation. The tools include a specification editor, a consistency checker, a simulator, and tools for verifying application properties including a model checker, a verifier, a property checker based on decision procedures, and an invariant generator. The paper also describes the practical systems to which the tools are being applied as well as some new tools recently added to the toolset, e.g. a tool that constructs a sound and complete abstraction from a property and a specification. To illustrate the tools, the paper describes their use in developing a requirements specification for an automobile cruise control system.