Formal methods for verification and validation of partial specifications: A case study |
| |
Authors: | Steve Easterbrook John Callahan |
| |
Affiliation: | NASA/WVU Software Research Lab, NASA Independent Verification and Validation Facility, 100 University Drive, Fairmont, WV 26554, USA |
| |
Abstract: | This paper describes our work exploring the suitability of formal specification methods for independent verification and validation (IV&V) of software specifications for large, safety-critical systems. An IV&V contractor often has to perform rapid analysis on incomplete specifications, with no control over how those specifications are represented. Lightweight formal methods show significant promise in this context, as they offer a way of uncovering major errors without the burden of full proofs of correctness. We describe a case study of the use of partial formal models for IV&V of the requirements for Fault Detection Isolation and Recovery on the space station. We conclude that the insights gained from formalizing a specification are valuable, and it is the process of formalization, rather than the end product, that is important. It was only necessary to build enough of the formal model to test the properties in which we were interested. Maintenance of fidelity between multiple representations of the same requirements (as they evolve) is still a problem, and deserves further study. |
| |
Keywords: | |
本文献已被 ScienceDirect 等数据库收录! |
|