{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/106202"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/106202","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Formal methods for safe autonomy: Data-driven verification, synthesis, and applications","abstract":"DSpace SAF Submission Ingestion Package generated from Vireo submission #14581 on 2020-02-28 at 17:13:55","abstract_html":"DSpace SAF Submission Ingestion Package generated from Vireo submission #14581 on 2020-02-28 at 17:13:55","abstract_has_math":false,"creators":["Fan, Chuchu"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Electrical & Computer Engr","degree_department":null,"school":null,"contributors":["Mitra, Sayan","Liberzon, Daniel","Murray, Richard","Sanders, William","Viswanathan, Mahesh"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2020,"date_issued":"2020-03-02T21:58:14Z","date_published":"2020-03-02T21:58:14Z","updated_at":"2026-07-22T22:24:45Z","subjects":["Autonomous systems","formal methods","verification","synthesis"],"languages":["en"],"rights":["Copyright 2019 Chuchu Fan"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/106202","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Mitra, Sayan","Liberzon, Daniel","Murray, Richard","Sanders, William","Viswanathan, Mahesh"]},{"key":"dc:creator","label":"Author","values":["Fan, Chuchu"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2020-03-02T21:58:14Z","2019-11-21","2019-12"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Electrical & Computer Engr"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Autonomous systems","formal methods","verification","synthesis"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2019 Chuchu Fan"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/106202"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["DSpace SAF Submission Ingestion Package generated from Vireo submission #14581 on 2020-02-28 at 17:13:55","Made available in DSpace on 2020-03-02T21:58:14Z (GMT). No. of bitstreams: 4 FAN-DISSERTATION-2019.pdf: 2819507 bytes, checksum: 91e7c9e5f2f905650f247531572f1eda (MD5) latex source.zip: 9131843 bytes, checksum: ea997ae8a64df7fefc4d18e406cdec73 (MD5) LICENSE.txt: 4207 bytes, checksum: 75ab5546952b8edc3df80b1c33cbdfe3 (MD5) PROQUEST_LICENSE.txt: 4553 bytes, checksum: 3cca95327033e0f66c377e198da7d354 (MD5) Previous issue date: 2019-11-21","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.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2020-02-28 without embargo terms","The student, Chuchu Fan, accepted the attached license on 2019-11-21 at 13:02.","The student, Chuchu Fan, submitted this Dissertation for approval on 2019-11-21 at 13:16.","This Dissertation was approved for publication on 2019-11-21 at 16:49."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Formal methods for safe autonomy: Data-driven verification, synthesis, and applications"]}]}],"canonical_facts":{"dc:contributor":["Mitra, Sayan","Liberzon, Daniel","Murray, Richard","Sanders, William","Viswanathan, Mahesh"],"dc:creator":["Fan, Chuchu"],"dc:date":["2020-03-02T21:58:14Z","2019-11-21","2019-12"],"dc:description":["DSpace SAF Submission Ingestion Package generated from Vireo submission #14581 on 2020-02-28 at 17:13:55","Made available in DSpace on 2020-03-02T21:58:14Z (GMT). No. of bitstreams: 4 FAN-DISSERTATION-2019.pdf: 2819507 bytes, checksum: 91e7c9e5f2f905650f247531572f1eda (MD5) latex source.zip: 9131843 bytes, checksum: ea997ae8a64df7fefc4d18e406cdec73 (MD5) LICENSE.txt: 4207 bytes, checksum: 75ab5546952b8edc3df80b1c33cbdfe3 (MD5) PROQUEST_LICENSE.txt: 4553 bytes, checksum: 3cca95327033e0f66c377e198da7d354 (MD5) Previous issue date: 2019-11-21","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.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2020-02-28 without embargo terms","The student, Chuchu Fan, accepted the attached license on 2019-11-21 at 13:02.","The student, Chuchu Fan, submitted this Dissertation for approval on 2019-11-21 at 13:16.","This Dissertation was approved for publication on 2019-11-21 at 16:49."],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/106202"],"dc:language":["en"],"dc:rights":["Copyright 2019 Chuchu Fan"],"dc:subject":["Autonomous systems","formal methods","verification","synthesis"],"dc:title":["Formal methods for safe autonomy: Data-driven verification, synthesis, and applications"],"dc:type":["text"],"thesis:degree_discipline":["Electrical & Computer Engr"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:24:45Z"}