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.

A formal verification of the transient fault recovery aspects of the Reliable Computing Platform (RCP), a fault-tolerant computing system architecture for digital flight control applications, is described. The RCP uses NMR-style redundancy to mask faults and internal majority voting to purge the effects of transient faults. The system design has been formally specified and verified using the EHDM verification system. The present formalization accommodates a wide variety of voting schemes for purging the effects of transients.>

Formal verification tools and techniques are difficult and expensive to apply. To make verification of large, complex systems more practical, TRW is developing the deductive theory manager (DTM). A knowledge-based tool that integrates with the Gypsy verification environment (GVE), the DTM supports the construction of deductive theories and applies them to proofs. Knowledge bases applicable to a variety of projects, and one specific to the army secure operating system (ASOS) proofs, are simultaneously under development. The authors describe the underlying philosophy of the verification strategy on which the DTM is based, present the DTM architecture, and illustrate DTM knowledge engineering and proof processing with a case study.>

The Army Secure Operating System (ASOS) program is providing a family of operating systems for tactical data system applications in Ada. Two members of the ASOS family have been developed: a dedicated secure operating system intended for the TCSEC (the DoD Trusted Computer System Evaluation Criteria) C2 level, and a multilevel secure operating system intended for the TCSEC A1 level. An overview is presented of the A1 system concept and TRW's solution to the ASOS kernel verification problem. A description is given of the model, the formal top-level specification :(FTLS), and proof approaches as well as some practical techniques for coping with proof complexity. Summary statistics on the actual proofs have been compiled and included in the discussion of the verification results.>