Example Applications of Formal Methods to Aerospace and Autonomous Systems

As systems become more complex, they become more difficult to verify. Testing is the most common verification approach, but testing can only cover a relatively small proportion of total system behaviors. In the aerospace domain, the time and cost required to run enough tests to adequately verify avionics is already a major issue, and it is anticipated to be an even bigger issue for autonomous systems. Formal methods, i.e. mathematically-based tools and approaches for system specification, design, and analysis-based verification, can potentially supplement test-based verification to provide better coverage of system behaviors in a more reasonable amount of time and at a more reasonable cost. However, the uptake of formal methods has been slow. Our experience interacting with several communities focused on verification and certification of aerospace and autonomous systems is that there are still frequently basic questions about what formal methods are, how they work, and what types of properties they can analyze, along with concerns that formal methods may not be realistic or mature. To help answer these questions and address these concerns, this paper provides a brief overview of formal methods and reviews a set of applications to aerospace and autonomous systems that demonstrate some types of systems and properties that formal methods are well-suited to verify, where they are mature, and where they are gaining in maturity.