Model Checking Autonomy Models for a Martian Propellant Production Plant

Model-Based Validation of Intelligence

Volume

Papers from the 2001 AAAI Spring Symposium

Contents

Expanded exploration of our Solar System will require more sophisticated autonomous assets to be developed and deployed. Model based autonomous control systems are a primary technology solution to this problem. A critical factor in the successful operations of these systems is to ensure that the models behave correctly. The Kennedy Space Center (KSC) has been pursing in conjunction with Ames Research Center the application of model-checking techniques for an Intelligent Systems Software for an In-Situ Resource Utilization (ISRU) plant for future manned Mars missions. Model checking is a formal technique which can exhaustively evaluate a finite state model for satisfiability of a logical property. The main goal of our current model checking effort is to develop tools and methodologies for efficient evaluation and certification of future Livingstone modeling applications which are declarative in form. As a result of this investigation a potential new re-usable specification pattern was derived which allows one to check a model for the existence of correct variable dependencies within the model.