Formal Methods for Trusted Space Autonomy, Boon or Bane?

Trusted Space Autonomy is challenging in that space systems are complex artifacts deployed in a high stakes environment with complicated operational settings. Thus far these challenges have been met using the full arsenal of tools: formal methods, informal methods, testing, runtime techniques, and operations processes. Using examples from previous deployments of autonomy to the Remote Agent on DS-1, Autonomous Sciencecraft on EO-1, WATCH on MER, IPEX, AEGIS on MER, MSL, and M2020, and the M2020 Onboard planner, we discuss how each of these approaches have been used to enable successful deployment of autonomy. We next focus on relatively limited use of formal methods (both prior to deployment and runtime methods). From the needs perspective, formal methods represent the best chance for reliable autonomy as testing, informal methods, and operations accommodations do not scale well with increasing complexity of the autonomous system. However from the practice perspective, formal methods have been limited in their application due to difficulty in eliciting formal specifications and challenges in representing complex constraints such as metric time and resources. We discuss some of these challenges as well as the opportunity to extend formal and informal methods into runtime validation systems.