FM Past Program: Space Applications
A team spread across three NASA centers was formed to study the application and technology transfer of formal methods to NASA space programs. A consortium of researchers and practitioners from LaRC, JSC, and JPL, together with support from Loral Space Information Systems, SRI International, and ViGYAN Inc., has been actively pursuing this objective since late 1992. The near term goal is to define and carry out pilot projects using portions of existing large-scale space programs. The long term goal is to enable organizations such as Loral to reduce formal methods to practice on programs of national importance.
The NASA Formal Methods Demonstration Project for Space Applications focuses on the use of formal methods for requirements analysis. It was thought that formal methods is more practically applied to requirements analysis than to late-lifecycle development phases. A series of trial projects was conducted and cost effectiveness data were collected. The team's efforts in 1993 were concentrated on a single pilot project, while later efforts in 1994 have been more diffuse.
The 1993 project was the formal specification of a very mature piece of the Space Shuttle flight control requirements called Jet Select. Initial specifications were written to capture an existing, low-level statement of the requirements. Few proofs were produced for the first specification, but 46 issues were identified and several minor errors were found in the requirements. A second specification was produced for an abstract (i.e., high level) representation of the Jet Select requirements. This abstraction, along with the 24 proofs of key properties, was accomplished in under 2 work months, and although it only uncovered 6 issues, several of these issues were significant.
NASA Langley's primary role in 1994 included support for two Space Shuttle software change requests (CR). One CR concerns the integration of new Global Positioning System (GPS) functions while the other concerns a new function to control contingency aborts known as Three Engine Out (3 E/O). Both of these tasks involved close cooperation among formal methods researchers at NASA Langley, ViGYAN Inc., and SRI International with requirements analysts from Lockheed-Martin (formerly Loral Space Information Systems).
The Space Shuttle is to be retrofitted with GPS receivers in anticipation of the TACAN navigation system being phased out by the DoD. Additional navigation software will be incorporated to process the position and velocity vectors generated by these receivers. A decision was made to focus the trial formal methods task on just a few key areas because the CR itself is very large and complex. A set of preliminary formal specifications was developed for the new Shuttle navigation principal functions known as GPS Receiver State Processing and GPS Reference State Processing, using the language of SRI's Prototype Verification System (PVS). While writing the formal specifications, 43 minor discrepancies were detected in the CR and these have been reported to Loral requirements analysts.
The Three Engine Out (3 E/O) Task is executed each cycle during powered flight until either a contingency abort maneuver is required or progress along the powered flight trajectory is sufficient to preclude a contingency abort even if three main engines fail. The 3 E/O task consists of two parts: 3 E/O Region Selection and 3 E/O Guidance. 3 E/O Region Selection is responsible for selecting the type of external tank (ET) separation maneuver and assigning the corresponding region index. 3 E/O guidance monitors ascent parameters and determines if an abort maneuver is necessary.
We have developed and analyzed a formal model of the series of sequential maneuvers that comprise the 3 E/O algorithm. To date, 20 potential issues have been found, including undocumented assumptions, logical errors, and inconsistent and imprecise terminology. These findings are listed as potential issues pending review by the 3 E/O requirements analyst.
In addition, NASA Langley has contributed to two volumes of a NASA Guidebook developed by the inter-center team. These guidebooks are available from the JPL formal methods page.
References
(These may be ordered)
-
National Aeronautics and Space Administration, Formal Methods Specification and Analysis Guidebook for the Verification of Software and Computer Systems, Volume II: A Practitioner's Companion , 1997, 245 pages.
-
National Aeronautics and Space Administration, Formal Methods Specification and Verification Guidebook for Software and Computer Systems, Volume I: Planning and Technology Insertion , July 1995, 77 pages.
- DiVito, Ben L.: Formalizing New Navigation Requirements for NASA's Space Shuttle , in Formal Methods Europe (FME '96), Oxford, England, March 1996.
- Crow, Judith; DiVito, Ben L.: Formalizing Space Shuttle Software Requirements, in First Workshop on Formal Methods in Software Practice San Diego, California, January 1996.
- Kelly, John; and Di Vito, Ben: Formal Methods Demonstration Project for Space Applications, Slides presented at the Third NASA Langley Formal Methods Workshop, May 10-12, 1995.