FORMAL METHODS FOR VERIFICATION AND VALIDATION OF PARTIAL SPECIFICATIONS - A CASE-STUDY

This paper describes our work exploring the suitability of formal spec ification 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 speci fications, with no control over how those specifications are represent ed. Lightweight formal methods show significant promise in this contex t, as they offer a way of uncovering major errors without the burden o f full proofs of correctness. We describe a case study of the use of p artial formal models for IV & V of the requirements for Fault Detectio n Isolation and Recovery on the space station. We conclude that the in sights gained from formalizing a specification are valuable, and it is the process of formalization, rather than the end product, that is im portant. It was only necessary to build enough of the formal model to test the properties in which we were interested. Maintenance of fideli ty between multiple representations of the same requirements (as they evolve) is still a problem, and deserves further study. (C) 1998 Elsev ier Science Inc.