Computer Systems: Science & Engineering · 2005 · 65 citations · 37 references
EngineeringComputer ScienceSystems EngineeringFormal MethodsRequirements EngineeringSoftware EngineeringRequirements AnalysisRequirements ElicitationRequirements ManagementRequirements SpecificationSoftware DesignSpecification DevelopmentCruise ControlCruise Control SystemsDecision ProceduresFormal Requirement SpecificationInvariant GenerationRequirements VerificationSoftware Requirements SpecificationSpecification Errors
Abstract : 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.
37
Graph-Based Algorithms for Boolean Function Manipulation
Bryant · IEEE Transactions on Computers · 1986 · 8.9K citations · Full text
Statecharts: a visual formalism for complex systems
David Harel · Science of Computer Programming · 1987 · 6.7K citations
Gerard J. Holzmann · IEEE Transactions on Software Engineering · 1997 · 3.8K citations