Building DryVR: A verification and controller synthesis engine for cyber-physical systems and safety-critical autonomous vehicle features

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.

Name thesis:degree_name

M.S.

Level thesis:degree_level

Thesis

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2018

Author dc:creator

• Qi, Bolun

Contributors dc:contributor

• Mitra, Sayan

• verification
• Cyber-pyhsical systems
• hybrid systems
• black-box
• controller synthesis

Statement dc:rights

• Copyright 2018 Bolun Qi

Language dc:language

en

Handle dc:identifier

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

OAI identifier oai:identifier

oai:www.ideals.illinois.edu:2142/101064