Item Details

Formal Specifications: A Systematic Evaluation

DeJong, Colleen; Gibble, Matthew; Knight, John; Nakano, Luis
DeJong, Colleen
Gibble, Matthew
Knight, John
Nakano, Luis
Industrial practitioners require constant improvements in the software development process and the quality of the resulting product in order to satisfactorily build larger and more complex systems. Academia praises formal specification techniques as a means to achieve these goals, yet formal specification has not been widely adopted by industry. The focus of this research is to study the disparity betweev industry and academia in their experience with formal specification methods. During the specification of a significant software system, a control system for a nuclear reactor, it became clear that the use of formal specification methods had potential benefits, but there were practical requirements thatt were not being met. Previous evaluations of formal specification failed to identify many of these flaws and a new comprehensive approach based on the requirements of the current software development process is needed. A comprehensive approach to evaluation was developed as part of this research. The evaluation method presented here does not examine theoretical qualities of language form and structure, rather it examines basic but vital practical issues involving the notation, tools, and methods for using them. There were two objectives of this research: - to identify these practical requirements and create a list of criteria for formal specification methods - to evaluate several formal specification methods based on these criteria. The criteria were systematically derived from current software development practice. This derivation links the criteria with specific activities in the software development process and supports their inclusion in the evaluation. Using this set of criteria, an evaluation of three formal specification methods, Z, PVS, and statecharts, was conducted by developing and examining specifications for a preliminary version of the reactor control system.
Date Received
University of Virginia, Department of Computer Science, 1997
Published Date
Libra Open Repository
Logo for In CopyrightIn Copyright


Access Online