Formal Specifications: A Systematic Evaluation

Authors:DeJong, Colleen, Department of Computer ScienceUniversity of Virginia Gibble, Matthew, Department of Computer ScienceUniversity of Virginia Knight, John, Department of Computer ScienceUniversity of Virginia Nakano, Luis, Department of Computer ScienceUniversity of Virginia

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.

All rights reserved (no additional license for public reuse)
Source Citation:

DeJong, Colleen, Matthew Gibble, John Knight, and Luis Nakano. "Formal Specifications: A Systematic Evaluation." University of Virginia Dept. of Computer Science Tech Report (1997).

University of Virginia, Department of Computer Science
Published Date: