 |
||
|
Advanced Search |
||
|
|||||
|
Requirements 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.
|
| Model Checking of Artificial Intelligence Based Planners | |
| Point of Contact |
Margaret Smith Margaret.H.Smith@jpl.nasa.gov |
| Dates | October 2003 - October 2007 |
| Problem | Our goal is to explore the suitability of logic model checking and specifically the model checking tool Spin to test Artificial Intelligence (AI) planning engines. AI planners are an enabling technology for autonomous control of spacecraft. Verification must ensure that the software will not endanger the mission under any circumstances. Traditional software testing samples a small subset of conditions that the AI planner will encounter. What is needed is a testing method that checks every possible combination of conditions under well thought out assumptions. Model checking is such a technique. It has been applied successfully to industrial projects to test the correctness of critical software components exhaustively. |
| Objective | By the end of the first full year we will have identified and classified the requirements on a specific AI engine (the MSL adaptation of the MDS software), created initial Spin models of the engine and its environment, and identified new tools/extensions needed. By the end of the second year, we will have created an initial version of tools/extensions, completed a library of reusable, formalized temporal requirements, finalized Spin models of the AI engine and its environment, and completed the model checking and reported faults to the development team. By the end of the third year, we will have completed a report of the model checking results, completed tool and method user documentation and guidelines for applying model checking to AI engines. |
| Results |
Identification of AI engine candidate risks.ppt Obtain-Configure MAP verification server.doc 2005 IEEE Aerospace conference paper.pdf SAS 06 Executive Presentation.ppt End of Year Briefing.ppt SAS 06 Technical Presentation.ppt Demonstration of Feasibility of addressing the risk using model checking on a 'toy' problem_MSmith.zip SAS 05 Executive Presentation_MSmith.ppt SAS 05 Technical Presentation_Model_Checking_AI_Based_Planners-MSmith.ppt Demonstration of Feasibility of addressing the risk using model checking on a real artifact of a past mission.zip SAS_07_Exec_Pres_Model_Chkg_AI_Smith_M.ppt SAS_07_Tech_Pres_Model_Chkg_AI_Smith_M.ppt |
| Keywords | Model checking, Artificial Intelligence, autonomy, testing |
| Categories |
Design Analysis Formal Methods Requirements Analysis |
|
| |
|
Curator: Josh Stonestreet NASA Official: Lisa Montgomery |
|
NASA Privacy, Security, Notices |