Results of a formal methods demonstration project

This paper describes the results of a cooperative study [D-11432] conducted by a team of researchers in formal methods (FM) at three NASA centers (The Jet Propulsion Laboratory (JPL), Johnson Space Center (JSC), and Langley Research Center (LaRC)) to demonstrate FM techniques and to tailor them to critical NASA software systems. FM is a set of techniques and tools based on formal logic and mathematics for the purpose of specifying and verifying computer systems and software. This pilot project applied FM to an existing critical software subsystem. The Shuttle´s Jet Select subsystem (Phase I of an ongoing study). The Prototype Verification System (PVS) specification language and tool developed at SRI International was used for this study. This study shows that FM can be used successfully to uncover hidden issues in a highly critical and mature Functional Subsystem Software Requirements (FSSR) specification which are very difficult to discover by traditional means