FM Past Program: Formal Specification of Space Shuttle Jet Select
This page is not maintained.
It is probably out of date.
NASA Langley worked with NASA Johnson Space Center and the
Jet Propulsion Laboratory (JPL) in a study to explore the feasibility and
utility of applying mechanically-supported formal methods to
requirements analysis for space applications.
The team worked with space application experts from NASA
Johnson, JPL, and IBM (now Loral) to
- educate the application experts about how to apply formal methods, and
about SRI's
PVS (Prototype Verification System)
- develop formal specifications
and prove simple properties of key software
subsystems for the
Jet Select function of the NASA
Space Shuttle
-
help interested groups such as JSC's Space Shuttle community move
toward realistic insertion of formal methods into their requirements
analysis process
Specifications were written at three different
levels of abstraction. The highest level specifications were proved
to meet a set of critical properties. This formal analysis uncovered
hidden problems in a highly critical and mature FSSR specification for
Shuttle. This project impressed several key members of the Shuttle
software community that the benefits of formal methods are concrete
and economically realizable. A very favorable reaction was received
from the IBM (now Loral) requirements analysts and senior JSC
personnel (Bob Hinson, in particular). They would like to work with
us ``to build a different paradigm where engineers write requirements
like this before passing the requirements to software development.''
This demonstration project was being funded by the Office of Safety and
Mission Quality at NASA Headquarters, which controls funding for
verification and validation of all major NASA space projects.
Curator and Responsible NASA Official: C. Michael Holloway
last modified: 22 February 1996 (13:01:17)
