Formal verification for a next-generation space shuttle

This paper discusses the verification and validation (V&V) of advanced software used for integrated vehicle health monitoring (IVHM), in the context of NASA's next-generation space shuttle. We survey the current V&V practice and standards used in selected NASA projects, review applicable formal verification techniques, and discuss their integration into existing development practice and standards. We also describe two verification tools, JMPL2SMV and Livingstone PathFinder, that can be used to thoroughly verify diagnosis applications that use model-based reasoning, such as the Livingstone system.