{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/101064"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/101064","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Building DryVR: A verification and controller synthesis engine for cyber-physical systems and safety-critical autonomous vehicle features","abstract":"To test safety of autonomous vehicles, large corporations have raced to log millions of miles of test driving on public roads. While this can improve confidence in such systems, testing alone cannot establish of absence of failure scenarios. In fact, it has also been reported that the amount of data required to guarantee a probability of 10^-9 fatality per hour of driving would require 10^9 hours of driving [1] [2], which is roughly in the order of thirty billion miles. Formal verification can give guarantees about absence of failures and potentially reduce the amount of testing needed significantly. Simulation based verification is a promising approach to provide formal safety guarantees to Cyber-Physical Systems (CPS). However, existing verification tools rely on the explicit mathematical models of the system. Detailed mathematical models are often not available or are too complex for formal verification tools. To address this issue, the DryVR approach for verification is presented in [3]. DryVR views a cyber-physical system as a combination of a white-box transition graph and a black-box simulator. This alleviates the need for complete mathematical models, but at the same time exploits models when they are available. A verification algorithm for directed acyclic time-dependent transition graph is also presented in [3]. In this thesis, we present the detailed construction of the DryVR tool with several new functionalities, which includes: (a) verification on state-dependent cyclic transition graph with guard and reset functions; (b) controller synthesis that searches transition graph for given reach-avoid specification; (c) interface that allows user to connect DryVR with arbitrary black-box simulators, and (d) integration with Jupyter Notebook [4]. We also present a case study for autonomous vehicle system in this thesis, and DryVR comes with verification and controller synthesis examples to illustrate its capabilities. The evaluation of included examples is presented in later chapter shows that both verification and controller synthesis are promising starting point for DryVR to become a comprehensive verification and synthesis toolbox for practical CPS.","abstract_html":"To test safety of autonomous vehicles, large corporations have raced to log millions of miles of test driving on public roads. While this can improve confidence in such systems, testing alone cannot establish of absence of failure scenarios. In fact, it has also been reported that the amount of data required to guarantee a probability of 10^-9 fatality per hour of driving would require 10^9 hours of driving [1] [2], which is roughly in the order of thirty billion miles. Formal verification can give guarantees about absence of failures and potentially reduce the amount of testing needed significantly. Simulation based verification is a promising approach to provide formal safety guarantees to Cyber-Physical Systems (CPS). However, existing verification tools rely on the explicit mathematical models of the system. Detailed mathematical models are often not available or are too complex for formal verification tools. To address this issue, the DryVR approach for verification is presented in [3]. DryVR views a cyber-physical system as a combination of a white-box transition graph and a black-box simulator. This alleviates the need for complete mathematical models, but at the same time exploits models when they are available. A verification algorithm for directed acyclic time-dependent transition graph is also presented in [3]. In this thesis, we present the detailed construction of the DryVR tool with several new functionalities, which includes: (a) verification on state-dependent cyclic transition graph with guard and reset functions; (b) controller synthesis that searches transition graph for given reach-avoid specification; (c) interface that allows user to connect DryVR with arbitrary black-box simulators, and (d) integration with Jupyter Notebook [4]. We also present a case study for autonomous vehicle system in this thesis, and DryVR comes with verification and controller synthesis examples to illustrate its capabilities. The evaluation of included examples is presented in later chapter shows that both verification and controller synthesis are promising starting point for DryVR to become a comprehensive verification and synthesis toolbox for practical CPS.","abstract_has_math":false,"creators":["Qi, Bolun"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"M.S.","degree_level":"Thesis","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Mitra, Sayan"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2018,"date_issued":"2018-09-04T20:31:54Z","date_published":"2018-09-04T20:31:54Z","updated_at":"2026-07-22T22:24:38Z","subjects":["verification","Cyber-pyhsical systems","hybrid systems","black-box","controller synthesis"],"languages":["en"],"rights":["Copyright 2018 Bolun Qi"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/101064","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Mitra, Sayan"]},{"key":"dc:creator","label":"Author","values":["Qi, Bolun"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2018-09-04T20:31:54Z","2018-04-25","2018-05"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["M.S."]},{"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":["verification","Cyber-pyhsical systems","hybrid systems","black-box","controller 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 2018 Bolun Qi"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/101064"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["To test safety of autonomous vehicles, large corporations have raced to log millions of miles of test driving on public roads. While this can improve confidence in such systems, testing alone cannot establish of absence of failure scenarios. In fact, it has also been reported that the amount of data required to guarantee a probability of 10^-9 fatality per hour of driving would require 10^9 hours of driving [1] [2], which is roughly in the order of thirty billion miles. Formal verification can give guarantees about absence of failures and potentially reduce the amount of testing needed significantly. Simulation based verification is a promising approach to provide formal safety guarantees to Cyber-Physical Systems (CPS). However, existing verification tools rely on the explicit mathematical models of the system. Detailed mathematical models are often not available or are too complex for formal verification tools. To address this issue, the DryVR approach for verification is presented in [3]. DryVR views a cyber-physical system as a combination of a white-box transition graph and a black-box simulator. This alleviates the need for complete mathematical models, but at the same time exploits models when they are available. A verification algorithm for directed acyclic time-dependent transition graph is also presented in [3]. In this thesis, we present the detailed construction of the DryVR tool with several new functionalities, which includes: (a) verification on state-dependent cyclic transition graph with guard and reset functions; (b) controller synthesis that searches transition graph for given reach-avoid specification; (c) interface that allows user to connect DryVR with arbitrary black-box simulators, and (d) integration with Jupyter Notebook [4]. We also present a case study for autonomous vehicle system in this thesis, and DryVR comes with verification and controller synthesis examples to illustrate its capabilities. The evaluation of included examples is presented in later chapter shows that both verification and controller synthesis are promising starting point for DryVR to become a comprehensive verification and synthesis toolbox for practical CPS.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2018-08-31 without embargo terms","The student, Bolun Qi, accepted the attached license on 2018-04-24 at 19:53.","The student, Bolun Qi, submitted this Thesis for approval on 2018-04-24 at 19:59.","This Thesis was approved for publication on 2018-04-25 at 15:32.","DSpace SAF Submission Ingestion Package generated from Vireo submission #12465 on 2018-08-31 at 17:14:36","Made available in DSpace on 2018-09-04T20:31:54Z (GMT). No. of bitstreams: 2 QI-THESIS-2018.pdf: 1037644 bytes, checksum: 82ba9fd0379239ccc3ff744dcab7ed05 (MD5) LICENSE.txt: 4205 bytes, checksum: c256fd6c2f42f2d9bbd37e53a7228cc9 (MD5) Previous issue date: 2018-04-25"]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Building DryVR: A verification and controller synthesis engine for cyber-physical systems and safety-critical autonomous vehicle features"]}]}],"canonical_facts":{"dc:contributor":["Mitra, Sayan"],"dc:creator":["Qi, Bolun"],"dc:date":["2018-09-04T20:31:54Z","2018-04-25","2018-05"],"dc:description":["To test safety of autonomous vehicles, large corporations have raced to log millions of miles of test driving on public roads. While this can improve confidence in such systems, testing alone cannot establish of absence of failure scenarios. In fact, it has also been reported that the amount of data required to guarantee a probability of 10^-9 fatality per hour of driving would require 10^9 hours of driving [1] [2], which is roughly in the order of thirty billion miles. Formal verification can give guarantees about absence of failures and potentially reduce the amount of testing needed significantly. Simulation based verification is a promising approach to provide formal safety guarantees to Cyber-Physical Systems (CPS). However, existing verification tools rely on the explicit mathematical models of the system. Detailed mathematical models are often not available or are too complex for formal verification tools. To address this issue, the DryVR approach for verification is presented in [3]. DryVR views a cyber-physical system as a combination of a white-box transition graph and a black-box simulator. This alleviates the need for complete mathematical models, but at the same time exploits models when they are available. A verification algorithm for directed acyclic time-dependent transition graph is also presented in [3]. In this thesis, we present the detailed construction of the DryVR tool with several new functionalities, which includes: (a) verification on state-dependent cyclic transition graph with guard and reset functions; (b) controller synthesis that searches transition graph for given reach-avoid specification; (c) interface that allows user to connect DryVR with arbitrary black-box simulators, and (d) integration with Jupyter Notebook [4]. We also present a case study for autonomous vehicle system in this thesis, and DryVR comes with verification and controller synthesis examples to illustrate its capabilities. The evaluation of included examples is presented in later chapter shows that both verification and controller synthesis are promising starting point for DryVR to become a comprehensive verification and synthesis toolbox for practical CPS.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2018-08-31 without embargo terms","The student, Bolun Qi, accepted the attached license on 2018-04-24 at 19:53.","The student, Bolun Qi, submitted this Thesis for approval on 2018-04-24 at 19:59.","This Thesis was approved for publication on 2018-04-25 at 15:32.","DSpace SAF Submission Ingestion Package generated from Vireo submission #12465 on 2018-08-31 at 17:14:36","Made available in DSpace on 2018-09-04T20:31:54Z (GMT). No. of bitstreams: 2 QI-THESIS-2018.pdf: 1037644 bytes, checksum: 82ba9fd0379239ccc3ff744dcab7ed05 (MD5) LICENSE.txt: 4205 bytes, checksum: c256fd6c2f42f2d9bbd37e53a7228cc9 (MD5) Previous issue date: 2018-04-25"],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/101064"],"dc:language":["en"],"dc:rights":["Copyright 2018 Bolun Qi"],"dc:subject":["verification","Cyber-pyhsical systems","hybrid systems","black-box","controller synthesis"],"dc:title":["Building DryVR: A verification and controller synthesis engine for cyber-physical systems and safety-critical autonomous vehicle features"],"dc:type":["text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["M.S."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:24:38Z"}