Formalizing space shuttle software requirements

Abstract
This article describes four case studies in which requirements for new flight software subsystems on NASA's Space Shuttle were analyzed using mechanically supported formal methods. Three of the studies used standard formal specification and verification techniques, and the fourth used state exploration. These applications illustrate two thesis: (1) formal methods complement conventional requirements analysis processes effectively and (2) formal methods confer benefits even when only selectively adopted and applied. The studies also illustrate the interplay of application maturity level and formal methods strategy, especially in areas such as technology transfer, legacy applications, and rapid formalization, and they raise interesting issues in problem domain modeling and in tailoring formal techniques to applications.

This publication has 8 references indexed in Scilit: