Title
Formal Verification for a Next-Generation Space Shuttle
Abstract
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.
Year
DOI
Venue
2002
10.1007/978-3-540-45133-4_5
Lecture Notes in Computer Science
Keywords
DocType
Volume
space shuttles,model based reasoning,software engineering,formal verification,verification and validation
Conference
2699
ISSN
Citations 
PageRank 
0302-9743
0
0.34
References 
Authors
8
3
Name
Order
Citations
PageRank
Stacy D. Nelson181.03
Charles Pecheur228428.50
dennis koga3121.81