Description: 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).

Benefits: Large-scale industrial control systems, in particular oil refineries, paper mills, and food processing plants, also maintain a large library of standard operating procedures which have been developed by system designers and installers. These must be adapted on a daily basis to the specific system configuration and product targets for manual or automatic execution. The SAFE-P technology will be directly applicable to ensuring that industrial plants' daily operating plans and scripts conform to the standard operating procedures. SAFE-P technology may also be applied when manually-operated industrial control systems are being transitioned to more automated control systems, to verify that newly-written executable control scripts conform to legacy manual (textual) operating procedures.

The proposed SAFE-P tool will be applicable to a wide variety of NASA missions including ISS, Shuttle, and Constellation operations. For manned and unmanned spacecraft operations, SAFE-P will bridge a critical gap in NASA's safety procedures, preventing the possibility of inadvertent commands that do not conform to standard operating procedures and that could lead to dangerous or even catastrophic consequences. SAFE-P fits directly within NASA's Automation for Operations (A4O) system concept, helping support significant reductions in operations costs and increases in operational efficiency while maintaining or improving system safety. The SAFE-P tool will be designed to integrate with NASA's Procedure Integrated Development Environment (PRIDE), seamlessly supporting efficient development of future executable procedures and scripts.