Formal Methods for Verification and Validation of Partial Specifications: A Case Study

Easterbrook, Steve; Callahan, John

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 V&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.

Document ID

19980017028

Acquisition Source

Ames Research Center

Document Type

Contractor Report (CR)

Authors

Date Acquired

September 6, 2013

Publication Date

July 28, 1997

Subject Category

Report/Patent Number

Funding Number(s)

Distribution Limits

Public

Work of the US Gov. Public Use Permitted.

Available Downloads

Name

Type

19980017028.pdf

STI

No Preview Available

NTRS

NTRS - NASA Technical Reports Server

Available Downloads

Related Records