SAFE-P: System for Assurance of Flight Executable Procedures

Award Information
Agency: National Aeronautics and Space Administration
Branch: N/A
Contract: NNX10CA17C
Agency Tracking Number: 085551
Amount: $599,924.00
Phase: Phase II
Program: SBIR
Awards Year: 2010
Solicitation Year: N/A
Solicitation Topic Code: X1
Solicitation Number: N/A
Small Business Information
211 N. First Street, Suite 300, Minneapolis, MN, 55401
DUNS: 103477993
HUBZone Owned: N
Woman Owned: N
Socially and Economically Disadvantaged: N
Principal Investigator
 David Musliner
 Principal Investigator
 (612) 612-9314
Business Contact
 David Musliner
Title: Sr. Principal Researcher
Phone: (612) 325-9314
Research Institution
NASA operates manned spacecraft according to rigorously-defined standard operating procedures. Unfortunately, operating procedures are often written in different languages. For example, Orion will use automatic procedures written in SCL, the Spacecraft Command Language, while backup manual procedures may be developed in PRL, the Procedure Representation Language. However, procedures developed in different languages may diverge, so that the backup PRL procedures do not operate in the same way as the SCL procedures. This could lead to unintended effects that may range from simply unexpected to inefficient or even catastrophic. We propose to develop the SAFE-P tool, which will use formal model-checking methods to prove that PRL and SCL procedures have the same underlying execution semantics. Our Phase 1 effort validated the effectiveness of our approach; Phase 2 will completely automate the model checking process and integrate with the Procedure Integrated Development Environment (PRIDE). SAFE-P will thus allow procedure authors to easily compare procedures as they are being developed. When differences are found by SAFE-P, they will be highlighted immediately in the PRIDE interface, allowing the operators to either fix problems or annotate the respective procedures to explain the differences. Using SAFE-P, NASA personnel will rapidly and confidently verify that if an automatic SCL program cannot be executed, a backup manual procedure in PRL will be equivalent and safe. Furthermore, as automatic translators are developed to transform procedures in one language into another NASA-relevant language (e.g., Tietronix's current effort to translate PRL into SCL), the SAFE-P tool will provide a critical validation mechanism to double-check the correctness of the translation and highlight areas where the translator makes mistakes (or deliberate approximations that yield different behavior).

* information listed above is at the time of submission.

Agency Micro-sites

SBA logo
Department of Agriculture logo
Department of Commerce logo
Department of Defense logo
Department of Education logo
Department of Energy logo
Department of Health and Human Services logo
Department of Homeland Security logo
Department of Transportation logo
Environmental Protection Agency logo
National Aeronautics and Space Administration logo
National Science Foundation logo
US Flag An Official Website of the United States Government