Model Checking Autonomy Models for a Martian Propellant Production Plant

Peter Engrand

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.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.