Testing Software Requirements with Z and Statecharts Applied to an Embedded Control System

摘要

Software development starts by specifying the requirements. A Software Requirements Specification (SRS) describes what the software must do. Naturally, the SRS takes the core role as the descriptive documentation at every phase of the development cycle. To avoid problems in the latter development phases and reduce life-cycle costs, it is crucial to ensure that the specification is correct. This paper describes how to model, test and evaluate (i.e., check, examine, and probe) a natural language (NL) SRS using two formalisms (Z and Statecharts). These formalisms are used to determine strategies for avoiding design defects that stem from the requirements that could ultimately lead to system failures. A case study was performed to validate the integrity of a Guidance Control SRS in terms of completeness, consistency, and fault-tolerance. Based on these experiences, the NL-specification → Z → Statechart transformations can be completed in a systematic and repeatable manner that yield valuable insight into the overall integrity of software specifications.