TY - GEN
T1 - Dryvr
T2 - 29th International Conference on Computer Aided Verification, CAV 2017
AU - Fan, Chuchu
AU - Qi, Bolun
AU - Mitra, Sayan
AU - Viswanathan, Mahesh
N1 - Funding Information:
M. Viswanathan—This work is supported by the grants CAREER 1054247 and CCF 1422798 from the National Science Foundation.
Publisher Copyright:
© Springer International Publishing AG 2017.
PY - 2017
Y1 - 2017
N2 - We present the DryVR framework for verifying hybrid control systems that are described by a combination of a black-box simulator for trajectories and a white-box transition graph specifying mode switches. The framework includes (a) a probabilistic algorithm for learning sensitivity of the continuous trajectories from simulation data, (b) a bounded reachability analysis algorithm that uses the learned sensitivity, and (c) reasoning techniques based on simulation relations and sequential composition, that enable verification of complex systems under long switching sequences, from the reachability analysis of a simpler system under shorter sequences. We demonstrate the utility of the framework by verifying a suite of automotive benchmarks that include powertrain control, automatic transmission, and several autonomous and ADAS features like automatic emergency braking, lane-merge, and auto-passing controllers.
AB - We present the DryVR framework for verifying hybrid control systems that are described by a combination of a black-box simulator for trajectories and a white-box transition graph specifying mode switches. The framework includes (a) a probabilistic algorithm for learning sensitivity of the continuous trajectories from simulation data, (b) a bounded reachability analysis algorithm that uses the learned sensitivity, and (c) reasoning techniques based on simulation relations and sequential composition, that enable verification of complex systems under long switching sequences, from the reachability analysis of a simpler system under shorter sequences. We demonstrate the utility of the framework by verifying a suite of automotive benchmarks that include powertrain control, automatic transmission, and several autonomous and ADAS features like automatic emergency braking, lane-merge, and auto-passing controllers.
UR - http://www.scopus.com/inward/record.url?scp=85026730578&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85026730578&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-63387-9_22
DO - 10.1007/978-3-319-63387-9_22
M3 - Conference contribution
AN - SCOPUS:85026730578
SN - 9783319633862
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 441
EP - 461
BT - Computer Aided Verification - 29th International Conference, CAV 2017, Proceedings
A2 - Kuncak, Viktor
A2 - Majumdar, Rupak
PB - Springer
Y2 - 24 July 2017 through 28 July 2017
ER -