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

Fan, Chuchu

Permalink

https://hdl.handle.net/2142/106202 Copy

Description

Title

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

Author(s)

Fan, Chuchu

Issue Date

2019-11-21

Director of Research (if dissertation) or Advisor (if thesis)

Mitra, Sayan

Doctoral Committee Chair(s)

Mitra, Sayan

Committee Member(s)

• Liberzon, Daniel
• Murray, Richard
• Sanders, William
• Viswanathan, Mahesh

Department of Study

Electrical & Computer Eng

Discipline

Electrical & Computer Engr

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Keyword(s)

• Autonomous systems
• formal methods
• verification
• synthesis

Abstract

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.

Graduation Semester

2019-12

Type of Resource

text

Permalink

http://hdl.handle.net/2142/106202

Copyright and License Information

Copyright 2019 Chuchu Fan

Owning Collections