 |
||
|
Advanced Search |
||
|
|||||
|
Domain-Specific Analysis < Verification & Validation < Results Home
|
|
Click here to complete a short survey. The results of this survey will be used to help us improve the research program and this website.
Click here to view research projects that had new research results added in the last 90 days.
|
| Runtime Continuous Verification of an Onboard Planner | |
| Point of Contact |
Jay Offut jayo@interfacecontrol.com |
| Dates | October 2002 - June 2004 |
| Problem | Onboard planners are coming. Several NASA and Air Force satellite programs are now leveraging a similar architecture that comprises of the scripting engine and expert system (SCL), the NASA Ames Livingstone model-based reasoner and an onboard plannersuch as the JPL CASPER or Europa, from NASA Ames. By nature, the number of plans that can be generated is infinite and cannot be exhaustively tested. Although extensive testing can be done on the ground, there is unfortunately no assurance that, under some unexpected conditions, the planner will not g enerate at runtime an unexpected/untested sequence of activities that could be harmful to the mission. The verification and validation of those cooperative and reactive components represent a new challenge that has to be addressed prior to flight. This is critical for mission success and mission assurance but also safety when used on man-flights such as shuttle or its upcoming replacement: the "Reusable Launch Vehicle (RLV2)". |
| Objective | Our objective is to verify at runtime that the sequences generated by the planner individually meet pre-defined safety specifications or sequence patterns. Hence, the burden is shifted from proving all execution traces correct, to only proving that the a ctually occurring execution traces are correct. This of course is much more practical, and may be the only way formal methods can be adopted for use in flight-missions in a scalable manner. |
| Results |
Overview Report.ppt CTL LTL Specifications for Runtime Plan Verification.doc FY04 End of Year Briefing.doc |
| Keywords | UML, safety, flight-missions, model-based |
| Categories |
Domain-Specific Analysis Dynamic Analysis Formal Methods |
|
| |
|
Curator: Josh Stonestreet NASA Official: Lisa Montgomery |
|
NASA Privacy, Security, Notices |