Formal methods for safe autonomy: Data-driven verification, synthesis, and applications

Autonomous systems are often safety-critical and are expected to work in uncertain environments. Ensuring design correctness and safety of autonomous systems has significant financial and legal implications. Existing design and test methodologies are inadequate for providing the needed level of safety assurances. Can formal methods provide certifiable trust or assurance for products with the vagaries of real-world autonomous systems? In this dissertation, we try to answer this question in the affirmative by developing new verification and synthesis algorithms, implementing them in software tools, and studying their performance on realistic applications. Verification and synthesis for typical models of real-world autonomous systems are well known to be theoretically undecidable, and approximate solutions are challenging due to their high dimensionality, nonlinearities, and their nondeterministic and hybrid nature. In addressing these challenges, we present (a) data-driven algorithmic verification via reachability analysis of nonlinear hybrid systems and (b) controller synthesis for high-dimensional linear systems under disturbances. The key technical developments within this theme include: (1) The first algorithm for over-approximating reach sets of general nonlinear models with locally optimal tightness guarantees. (2) A novel verification framework that can tackle systems with incomplete models, by treating them as combinations of a “white-box” control graph and “black-box” simulators. We also provide a learning-based verification algorithm to provide probabilistic guarantees. (3) An approximate partial order reduction method to exponentially reduce the number of executions to be explored for reachability analysis of nondeterministic models of distributed systems. (4) An algorithm to find a combined open-loop controller and tracking controller for high-dimensional linear systems to meet reach-avoid specifications. On the theoretical front, the techniques are armed with soundness, precision, and relative completeness guarantees. On the experimental side, we show that the techniques can be successfully applied on a sequence of challenging problems, including a suite of Toyota engine control models verified for the first time, satellite control systems, and autonomous driving and ADAS-based maneuvers