Model checking autonomy models for a martian propellant production plant

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 certificatio