Files in this item



application/pdfQI-THESIS-2018.pdf (1MB)
(no description provided)PDF


Title:Building DryVR: A verification and controller synthesis engine for cyber-physical systems and safety-critical autonomous vehicle features
Author(s):Qi, Bolun
Advisor(s):Mitra, Sayan
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Cyber-pyhsical systems
hybrid systems
controller synthesis
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.
Issue Date:2018-04-25
Rights Information:Copyright 2018 Bolun Qi
Date Available in IDEALS:2018-09-04
Date Deposited:2018-05

This item appears in the following Collection(s)

Item Statistics