Source-linked AI summary
DRYVR:Data-driven verification and compositional reasoning for automotive systems
Chuchu Fan, Bolun Qi, Sayan Mitra, Mahesh Viswanathan
TL;DR
Hybrid-system verification often assumes clean mathematical models, although real control systems may be difficult to model that way. DryVR combines a black-box simulator with a white-box transition graph and learned sensitivity; it verified or found counterexamples for stated automotive benchmarks in minutes and inferred safety under arbitrary transitions and duration.
Problem
Many real-world control systems mix heterogeneous descriptions, making clean mathematical models usually infeasible to extract for verification.
Source: §1 · p. 1Method
DryVR combines a black-box simulator for continuous trajectories with a white-box transition graph, learns trajectory sensitivity from simulations, and applies reachability and graph-based reasoning.
Source: §1 · p. 2, Safety verification algorithm · p. 2, §2.2.1 · p. 5Results
DryVR verified or found counterexamples for all stated automotive benchmark scenarios in minutes, with reachability and compositional reasoning supporting safety under arbitrary transitions and duration.
Source: Safety verification algorithm · p. 3Takeaways & Limitations
The framework offers a way to analyze automotive control systems over long switching sequences using simulation and compositional reasoning.
Source: §5 · p. 17The implementation depends on Simulink, and the authors report that the lack of a public MathWorks license prevents releasing the tool at this stage.
Source: §3.3 · p. 13
Abstract
from arXiv · showhide
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.
1 Introduction
DryVR targets hybrid control systems whose continuous dynamics are hard to describe mathematically by combining black-box simulation with white-box mode-switch graphs. It uses learned trajectory sensitivity and graph-based reasoning to verify automotive systems, including under long switching sequences.
1 Introduction
- Real-world control systems combine simulation code, equations, block diagrams, and lookup tables, making clean mathematical models usually infeasible to extract.Source: §1 · p. 1
- DryVR represents hybrid systems with a white-box transition graph for mode switches and a black-box simulator for continuous trajectories in each mode.Source: §1 · p. 2
- A probabilistic learner estimates exponential discrepancy-function parameters from simulation data, enabling sound bounded reachability analysis when the learned discrepancy is correct.The learning problem is transformed into finding a linear separator; experiments found 15–20 traces typically yielded a discrepancy function working for nearly 100% of simulations.Source: Safety verification algorithm · p. 2
- Forward simulation between transition graphs provides a sufficient condition for reachable-state containment, so safety under the subsuming graph implies safety under the other graph.Source: Safety verification algorithm · p. 3
- Sequential composition concatenates switching sequences, and a sufficient condition lets safety under one graph imply safety under arbitrarily many repetitions of that graph.The analyzed transition graphs are acyclic and have bounded switching times.Source: Safety verification algorithm · p. 3
- DryVR verified or found counterexamples for all stated automotive benchmarks in minutes, with reachability and compositional reasoning supporting safety under arbitrary transitions and duration.Source: Safety verification algorithm · p. 3
2 Modeling/semantic framework
The framework formalizes hybrid systems by pairing a graph of mode switches with mode-labeled continuous trajectories, illustrated through a powertrain model.
2.1 Powertrain control system
- The Powertrn example models a nonlinear engine with four modes and Simulink dynamics; one requirement keeps the air-fuel ratio within a desired range under driver profiles.The requirement has implications for fuel economy and emissions.Source: §2.1 · p. 4, §2 · p. 4
2.2 Transition graphs
- A transition graph is a labeled directed acyclic graph whose vertices name modes and whose edges carry bounded, nonempty time intervals; maximal paths define allowed mode-and-time traces.Source: §2.2 · p. 4
2.2.1 Trace containment
- Trace containment requires each mapped trace of G1 to be a prefix of a G2 trace; a forward simulation relation is sufficient to establish it.Source: §2.2.1 · p. 5
2.2.2 Sequential composition of graphs
- Sequential composition concatenates compatible graphs, and every path of G1 remains a prefix of a path in G1 ◦ G2.Source: §2.2.2 · pp. 5–6
2.3 Trajectories
- DryVR uses sampled simulator or test trajectories rather than requiring generating equations; simulator queries return trajectory states, with perfect simulations assumed or validated simulations permitted.Source: §2.3 · p. 6
2.4 Hybrid systems
- Hybrid executions follow graph-allowed mode sequences and continuous trajectories; bounded safety checks whether reachable states intersect the unsafe set, while reachability containment follows from initial, graph, and trajectory containment.Source: §2.4 · pp. 7–8
2.5 ADAS and autonomous vehicle benchmarks
- ADAS benchmarks combine black-box Simulink vehicle dynamics with graph-encoded decisions and require safe separation across merge, auto-passing, Merge3, and AEB scenarios.Source: §2.5 · p. 8
3 Invariant verification
The section learns trajectory sensitivity from simulations to construct reach tubes for hybrid systems with black-box continuous dynamics. It combines this analysis with transition-graph reasoning to check safety and a class of temporal properties.
3.1 Discrepancy functions
- A probabilistic sampling method learns discrepancy functions from black-box simulations, enabling reach-tube approximation without a white-box ODE model.Discrepancy bounds trajectory separation and supports over-approximation from simulations.Source: §3 · p. 9, §3.1 · p. 9
3.1.2 Learning discrepancy functions
- GED uses one exponential bound over the time horizon, while PED learns interval-specific bounds and chooses intervals to keep each γ_i below 2.For Powertrn, PED produced a more precise reach tube; for the other benchmarks, GED and PED had comparable reach tubes and verification times.Source: §3.1.2 · pp. 10–11, §3.3 · p. 14
3.1.3 Experiments on learning discrepancy
- With more than 20 training traces, learned discrepancies were correct for more than 99.9% of tested points across the experiments.With more than 10 traces, they were correct for 96% of tested points.Source: §3.1.3 · p. 11
3.2 Verification algorithm
- GraphReach processes transition-graph vertices to compute reach tubes whose union over-approximates the system’s reachable tube.It learns a discrepancy for each initial set and mode, then uses simulated traces and that discrepancy to construct a reach tube.Source: §3.2 · pp. 11–12
- VerifySafety checks whether over-approximated reach tubes intersect the unsafe set, refining them when needed; DryVR also handles properties timed from the last mode transition.The stated soundness guarantee applies when the learned discrepancy functions are correct; the temporal-property example checks air-fuel-ratio bounds after four seconds in specified modes.Source: §3.2 · pp. 12–13
3.3 Experiments on safety verification
- The implementation depends on Simulink, and the authors report that licensing and integration complexity prevented releasing DryVR at that stage.They planned release after moving the black-box benchmarks to open-source software.Source: §3.3 · p. 13
- All benchmark analyses terminated in a few minutes, including simulation, discrepancy learning, reach-tube generation, safety checks, and refinements.The reported Table 1 results use global exponential discrepancy (GED).Source: Table 1 · p. 14, §3.3 · p. 14
- For AutoPassing, the unsafe set was disjoint from the computed reach tube for one initial set, while DryVR found a counterexample for another.The safe case has syA ∈ [0, 2] and syB ∈ [15, 17]; the counterexample case uses syB ∈ [30, 40].Source: §3.3 · pp. 13–14
4 Reasoning principles for trace containment
The section develops graph-containment and sequential-composition rules for transferring safety results from simpler transition graphs to more complex ones. Its examples apply these rules to AEB and powertrain systems.
4 Reasoning principles for trace containment
- Trace containment transfers reachability containment, so safety of the system with the larger reachable set implies safety of the other system.The argument relies on containment of traces, trajectories, and initial sets.Source: §4 · p. 14
- Forward simulation between transition graphs is a sufficient, polynomial-time-checkable condition for trace containment.The section notes that timed-language containment is decidable but its cited algorithm has non-elementary complexity.Source: §4 · p. 15
- Sequential composition preserves trace containment when each component graph is contained in its corresponding graph.The section also identifies a semigroup property for sequential composition.Source: §4 · p. 15
- The reach set under sequential composition is the union of the reach sets for the first graph and the continuation from its terminal state.This decomposition underpins the repeated-composition reasoning.Source: §4 · p. 16
- Theorem 4.4 supports safety verification for repeated switching sequences from a single-copy analysis when its stated condition holds.The result extends to replacing a repeated middle graph block by one copy within a larger composition.Source: §4 · p. 16
4.1 Experiments on trace containment reasoning
- AEB reachtubes for the simpler graph G1 contain those for the actual two-trigger graph G2.The example checks G2 ⪯id G1, making verification of G1 adequate to infer safety for G2.Source: §4.1 · pp. 16–17, Figure 3 · p. 17
- Powertrain analysis of GA ◦ GB sufficed to verify GA ◦ GB ◦ GB ◦ GB, and DryVR also proved the longer graph safe without refinement.For the composed stages, the estimated λ range was 14.68–14.71 and the later reachset range was 14.69–14.70; remaining variables also met containment.Source: §4.1 · p. 17
5 Conclusions
The conclusion presents DRYVR as an alternative for hybrid systems lacking complete mathematical models. It summarizes its verification and reasoning contributions and points to more general white-box automata as future work.
5 Conclusions
- DRYVR treats hybrid systems as a black-box simulator paired with a white-box transition graph when complete mathematical models are unavailable.The conclusion describes a semantic framework, probabilistic verification algorithm, and reasoning results based on simulation relations and sequential composition.Source: §5 · p. 17
- The authors report modeling and analyzing automotive control systems using the proposed approach as evidence of its promise.Source: §5 · p. 17
- A future direction is extending the white-box model to more general timed and hybrid automata and developing the needed algorithms and reasoning techniques.Source: §5 · p. 17
A.1 ADAS and autonomous vehicle venchmarks
The appendix details ADAS and autonomous-driving scenarios as mode sequences, timing conditions, and safety requirements. The scenarios cover emergency braking, merging, and passing maneuvers.
A.1 ADAS and autonomous vehicle venchmarks
- The modeled vehicle scenarios use position and velocity variables in both road directions, with throttle and steering-speed inputs controlling the modes.The defined modes include cruise, speedup, braking, emergency braking, and left or right lane switching.Source: §A.1 · p. 23
- MergeBetween and MergeAhead use speedup and lane-change sequences, with requirements to merge behind or ahead of another vehicle while maintaining separation.MergeBetween also specifies that vehicle C remains ahead of A through its cruise-to-speedup-to-cruise sequence.Source: §A.1 · pp. 23–24
- AutoPassing requires vehicle A to overtake B with minimum safe separation and adjust or abort the maneuver under specified B-mode changes.The sequence includes lane changes, speedup, and braking; B speeding up can trigger an abort, while B braking can require a timing adjustment.Source: §A.1 · p. 23
- AEB requires vehicle A to stop behind a stationary vehicle B while maintaining a specified safe separation.The transition graph permits braking over one interval or several disjoint intervals.Source: §A.1 · pp. 23–24
A.2 Automatic transmission control
The automatic transmission benchmark is a modified Simulink demo modeled with white-box mode transitions and black-box simulations. Its verification target is an engine-speed safety requirement.
A.2 Automatic transmission control
- The benchmark is a slightly modified MathWorks Simulink automatic-transmission demo; the paper notes prior falsification work but no verification results known to its authors.The authors state that they verified it using DryVR’s safety-verification algorithm.Source: §A.2 · p. 24
- The ATS benchmark checks whether engine RPM stays below a specified maximum, with Erpm > 4000 given as a typical unsafe set.Source: §A.2 · p. 24
- The modeled controller shifts across four modes—gear1 through gear4—with transition sequences and intervals encoded in its graph.Simulations record car speed, engine RPM, impeller torque, output torque, and transmission RPM.Source: §A.2 · p. 24
A.3 Safety verification algorithm
Algorithm 2 verifies hybrid-system safety with respect to an unsafe set, following the line of simulation-based verification algorithms [22, 29, 23].
A.3 Safety verification algorithm
- The algorithm follows the line of simulation-based verification algorithms [22, 29, 23].Source: §A.3 · p. 24
- Algorithm 2 verifies safety of hybrid system H with respect to unsafe set U.Source: §A.3 · p. 25
- One branch checks whether a reachable tube is contained in unsafe set U.Source: §A.3 · p. 25