Proceedings of ISRE '97: 3rd IEEE International Symposium on Requirements Engineering (1997)
Jan. 5, 1997 to Jan. 8, 1997
Steve Easterbrook , NASA/ West Virginia University Software IV&V Facility
John Callahan , NASA/ West Virginia University Software IV&V Facility
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 an experiment in the application of the method SCR to testing for consistency properties of a partial model of the requirements for Fault Detection Isolation and Recovery on the space station. We conclude that the insights gained from formalizing a specification is 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.
J. Callahan and S. Easterbrook, "Formal Methods for V&V of Partial Specifications: An Experience RSeport," Proceedings of ISRE '97: 3rd IEEE International Symposium on Requirements Engineering(RE), Annapolis, MD, 1997, pp. 160.