Dryvr: Data-driven verification and compositional reasoning for automotive systems

Chuchu Fan, Bolun Qi, Sayan Mitra, Mahesh Viswanathan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 29th International Conference, CAV 2017, Proceedings
EditorsViktor Kuncak, Rupak Majumdar
PublisherSpringer-Verlag Berlin Heidelberg
Pages441-461
Number of pages21
ISBN (Print)9783319633862
DOIs
StatePublished - 2017
Event29th International Conference on Computer Aided Verification, CAV 2017 - Heidelberg, Germany
Duration: Jul 24 2017Jul 28 2017

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10426 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other29th International Conference on Computer Aided Verification, CAV 2017
CountryGermany
CityHeidelberg
Period7/24/177/28/17

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Dryvr: Data-driven verification and compositional reasoning for automotive systems'. Together they form a unique fingerprint.

Cite this