Model Checking the Remote Agent Planner

Verification and validation of autonomous spacecraft software is a critical problem. With more missions being designed and flown in a shorter span of time from mission conception to flight, traditional methods of validation and testing are struggling to remain effective. Model-based autonomous system software is potentially more complex since it strives to provide increased system robustness by correctly addressing a wider range of possible system behaviors. The modelbased approach facilitates the elicitation and automatic manipulation of system level constraints. However, the models used in this approach still need to be verified, i.e., it is necessary to guarantee that no unintended consequences will arise.