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

TL;DR

DRYVR is a framework that combines data-driven sensitivity analysis, probabilistic reachability, and compositional reasoning to verify complex hybrid automotive systems efficiently.

Contribution

It introduces a novel combination of simulation-based sensitivity learning and compositional verification techniques for hybrid control systems.

Findings

Successfully verified automotive benchmarks including powertrain and autonomous features.

Demonstrated effectiveness in handling long switching sequences in hybrid systems.

Provided scalable verification methods for complex automotive control systems.

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.

Tables

Table 1. Table 1 : Safety verification results. Numbers below benchmark names: # vertices and edges of G 𝐺 G , TH: duration of shortest path in G 𝐺 G , Ref: # refinements performed; Runtime: overall running time.

Model	TH	Initial set	$𝒰$	Ref	Safe	Runtime
$\mathrm{𝖯𝗈𝗐𝖾𝗋𝗍𝗋𝗇}$ (5 vers, 6 edges)	80	$\lambda \in [14.6,14.8]$	${𝒰}_p$	2	✓	217.4s
$\mathrm{𝖠𝗎𝗍𝗈𝖯𝖺𝗌𝗌𝗂𝗇𝗀}$	50	$s{y}_A\in [-1,1]$ $s{y}_B\in [14,16]$	${𝒰}_c$	4	✓	208.4s
(12 vers, 13 edges)	50	$s{y}_A\in [-1,1]$ $s{y}_B\in [4,6.5]$	${𝒰}_c$	5	✗	152.5s
$\mathrm{𝖬𝖾𝗋𝗀𝖾}$	50	$s{x}_A\in [-5,5]$ $s{y}_B\in [-2,2]$	${𝒰}_c$	0	✓	55.0s
(7 vers, 7 edges)	50	$s{x}_A\in [-5,5]$ $s{y}_B\in [2,10]$	${𝒰}_c$	-	✗	38.7s
$\mathrm{𝖬𝖾𝗋𝗀𝖾𝟥}$	50	$s{y}_A\in [-3,3]$ $s{y}_B\in [14,23]$ $s{y}_C\in [36,45]$	${𝒰}_c$	4	✓	197.6s
(6 vers, 5 edges)	50	$s{y}_A\in [-3,3]$ $s{y}_B\in [14,15]$ $s{y}_C\in [16,20]$	${𝒰}_c$	-	✗	21.3s
$\mathrm{𝖠𝖳𝖲}$ (4 vers, 3 edges)	50	Erpm $\in [900,1000]$	${𝒰}_t$	2	✓	109.2s

Equations

$$|{\tau }_1(t)-{\tau }_2(t)|\le \beta ({\tau }_1.fstate,{\tau }_2.fstate,t),$$

$$\forall (x,y)\in \Gamma .x\le ay+b.$$

$$\beta (x_1,x_2,t)=|x_1-x_2|K{e}^{\gamma t}.$$

$$\forall t\in [0,T].|{\tau }_1(t)-{\tau }_2(t)|\le |{\tau }_1.fstate-{\tau }_2.fstate|K{e}^{\gamma t}.$$

$$\forall t.\ln \frac{|{\tau }_1(t)-{\tau }_2(t)|}{|{\tau }_1.fstate-{\tau }_2.fstate|}\le \gamma t+\ln K.$$

$$\beta (x_1,x_2,t)=|x_1-x_2|K{e}^{{\sum }_{j=1}^{i-1}{\gamma }_j(t_j-t_{j-1})+{\gamma }_i(t-t_{i-1})}\text{mbox}fort\in [t_{i-1},t_i].$$

Full text

1 Introduction

The starting point of existing hybrid system verification approaches is the availability of nice mathematical models describing the transitions and trajectories. This central conceit severely restricts the applicability of the resulting approaches. Real world control system “models” are typically a heterogeneous mix of simulation code, differential equations, block diagrams, and hand-crafted look-up tables. Extracting clean mathematical models from these descriptions is usually infeasible. At the same time, rapid developments in Advanced Driving Assist Systems (ADAS), autonomous vehicles, robotics, and drones now make the need for effective and sound verification algorithms stronger than ever before. The DryVR framework presented in this paper aims to narrow the gap between sound and practical verification for control systems.

Model assumptions

Consider an ADAS feature like automatic emergency braking system (AEB). The high-level logic deciding the timing of when and for how long the brakes are engaged after an obstacle is detected by sensors is implemented in a relatively clean piece of code and this logical module can be seen as a white-box. In contrast, the dynamics of vehicle itself, with hundreds of parameters, is more naturally viewed as a black-box. That is, it can be simulated or tested with different initial conditions and inputs, but it is nearly impossible to write down a nice mathematical model.

The empirical observation motivating this work is that many control systems, and especially automotive systems, share this combination of white and black boxes (see other examples in Sections 2.1, 2.5, and A.2). In this paper, we view hybrid systems as a combination of a white-box that specifies the mode switches and a black-box that can simulate the continuous evolution in each mode. Suppose the system has a set of modes ${\mathcal{L}}$ and $n$ continuous variables. The mode switches are defined by a transition graph $G$ which is a directed acyclic graph (DAG) whose vertices and edges define the allowed mode switches and the switching times. The black-box is a set of trajectories $\mathcal{T\mkern-3.0muL}$ in ${\mathbb{R}}^{n}$ for each mode in ${\mathcal{L}}$. We do not have a closed form description of $\mathcal{T\mkern-3.0muL}$, but instead, we have a simulator, that can generate sampled data points on individual trajectories for a given initial state and mode. Combining a transition graph $G$, a set of trajectories $\mathcal{T\mkern-3.0muL}$, and a set of initial states in ${\mathbb{R}}^{n}$, we obtain a hybrid system for which executions, reachability, and trace containment can be defined naturally.

We have studied a suite of automotive systems such as powertrain control [40], automatic transmission control [46], and ADAS features like automatic emergency braking (AEB), lane-change, and auto-passing, that are naturally represented in the above style. In verifying a lane change or merge controller, once the maneuver is activated, the mode transitions occur within certain time intervals. In testing a powertrain control system, the mode transitions are brought about by the driver and it is standard to describe typical driver classes using time-triggered signals. Similar observations hold in other examples.

Safety verification algorithm

With black-box modules in our hybrid systems, we address the challenge of providing guaranteed verification. Our approach is based on the idea of simulation-driven reachability analysis [30, 22, 23]. For a given mode $\ell\in{\mathcal{L}}$, finitely many simulations of the trajectories of $\ell$ and a discrepancy function bounding the sensitivity of these trajectories, is used to over-approximate the reachable states. For the key step of computing discrepancy for modes that are now represented by black-boxes, we introduce a probabilistic algorithm that learns the parameters of exponential discrepancy functions from simulation data. The algorithm transforms the problem of learning the parameters of the discrepancy function to the problem of learning a linear separator for a set of points in ${\mathbb{R}}^{2}$ that are obtained from transforming the simulation data. A classical result in PAC learning, ensures that any such discrepancy function works with high probability for all trajectories. We performed dozens of experiments with a variety of black-box simulators and observed that 15-20 simulation traces typically give a discrepancy function that works for nearly 100% of all simulations. The reachability algorithm for the hybrid system proceeds along the vertices of the transition graph in a topologically sorted order and this gives a sound bounded time verification algorithm, provided the learned discrepancy function is correct.

Reasoning

White-box transition graphs in our modelling, identify the switching sequences under which the black-box modules are exercised. Complex systems have involved transition graphs that describe subtle sequences in which the black-box modules are executed. To enable the analysis of such systems, we identify reasoning principles that establish the safety of system under a complex transition graph based on its safety under a simpler transition graph. We define a notion of forward simulation between transition graphs that provides a sufficient condition of when one transition graph “subsumes” another — if $G_{1}$ is simulated by $G_{2}$ then the reachable states of a hybrid system under $G_{1}$ are contained in the reachable states of the system under $G_{2}$. Thus the safety of the system under $G_{2}$ implies the safety under $G_{1}$. Moreover, we give a simple polynomial time algorithm that can check if one transition graph is simulated by another.

Our transition graphs are acyclic with transitions having bounded switching times. Therefore, the executions of the systems we analyze are over a bounded time, and have a bounded number of mode switches. An important question to investigate is whether establishing the safety for bounded time, enables one can conclude the safety of the system for an arbitrarily long time and for arbitrarily many mode switches. With this in mind, we define a notion of sequential composition of transition graphs $G_{1}$ and $G_{2}$, such that switching sequences allowed by the composed graph are the concatenation of the sequences allowed by $G_{1}$ with those allowed by $G_{2}$. Then we prove a sufficient condition on a transition graph $G$ such that safety of a system under $G$ implies the safety of the system under arbitrarily many compositions of $G$ with itself.

Automotive applications

We have implemented these ideas to create the Data-driven System for Verification and Reasoning (DryVR). The tool is able to automatically verify or find counter-examples in a few minutes, for all the benchmark scenarios mentioned above. Reachability analysis combined with compositional reasoning, enabled us to infer safety of systems with respect to arbitrary transitions and duration.

Related work

Most automated verification tools for hybrid systems rely on analyzing a white-box mathematical model of the systems. They include tools based on decidablity results [13, 37, 10, 3, 24, 32], semi-decision procedures that over-approximate the reachable set of states through symbolic computation [36, 48, 7, 45, 56, 33, 4, 9], using abstractions [1, 12, 11, 19, 55, 53, 16, 39, 52, 5, 6, 49, 54], and using approximate decision procedures for fragments of first-order logic [44]. More recently, there has been interest in developing simulation-based verification tools [41, 18, 17, 42, 2, 25, 15, 23]. Even though these are simulation based tools, they often rely on being to analyze a mathematical model of the system. The type of analysis that they rely on include instrumentation to extract a symbolic trace from a simulation [42], stochastic optimization to search for counter-examples [2, 25], and sensitivity analysis [18, 17, 15, 23]. Some of the simulation based techniques only work for systems with linear dynamics [34, 35]. Recent work on the APEX tool [50] for verifying trajectory planning and tracking in autonomous vehicles is related our approach in that it targets the same application domain.

2 Modeling/semantic framework

We introduce a powertrain control system from [40] as a running example to illustrate the elements of our hybrid system modeling framework.

2.1 Powertrain control system

This system (${\operatorname{\mathsf{Powertrn}}}$) models a highly nonlinear engine control system. The relevant state variables of the model are intake manifold pressure ($p$), air-fuel ratio ($\lambda$), estimated manifold pressure ($pe$) and intergrator state ($i$). The overall system can be in one of four modes ${\sf{startup}}$, ${\sf{normal}}$, ${\sf{powerup}}$, ${\sf{sensorfail}}$. A Simulink® diagram describes the continuous evolution of the above variables. In this paper, we mainly work on the Hybrid I/O Automaton Model in the suite of powertrain control models. The Simulink® model consists of continuous variables describing the dynamics of the powertrain plant and sample-and-hold variables as the controller. One of the key requirements to verify is that the engine maintains the air-fuel ratio within a desired range in different modes for a given set of driver behaviors. This requirement has implications on fuel economy and emissions. For testing purposes, the control system designers work with sets of driver profiles that essentially define families of switching signals across the different modes. Previous verification results on this problem have been reported in [21, 27] on a simplified version of the powertrain control model.

2.2 Transition graphs

We will use ${\mathcal{L}}$ to denote a finite set of modes or locations of the system under consideration. The discrete behavior or mode transitions are specified by what we call a transition graph over ${\mathcal{L}}$.

Definition 2.1**.**

A transition graph is a labeled, directed acyclic graph $G=\langle{\mathcal{L}},{\mathcal{V}},{\mathcal{E}},{\sc vlab},{\sc elab}\rangle$, where

(a) ${\mathcal{L}}$is the set of vertex labels also called the set of modes,

(b) ${\mathcal{V}}$the set of vertices,

(c) ${\mathcal{E}}\subseteq{\mathcal{V}}\times{\mathcal{V}}$is the set of edges,

(d) ${\sc vlab}:{\mathcal{V}}\rightarrow{\mathcal{L}}$is a vertex labeling function that labels each vertex with a mode, and

(e) ${\sc elab}:{\mathcal{E}}\rightarrow{{\mathbb{R}}_{\geq 0}}\times{{\mathbb{R}}_{\geq 0}}$is an edge labeling function that labels each edge with a nonempty, closed, bounded interval defined by pair of non-negative reals.

Since $G$ is a DAG, there is a nonempty subset ${\mathcal{V}}_{\sf init}\subseteq{\mathcal{V}}$ of vertices with no incoming edges and a nonempty subset ${\mathcal{V}}_{\sf term}\subseteq{\mathcal{V}}$ of vertices with no outgoing edges. We define the set of initial locations of $G$ as ${\mathcal{L}}_{\sf init}=\{\ell\ |\ \exists\ v\in{\mathcal{V}}_{\sf init},{\sc vlab}(v)=\ell\}$. A (maximal) path of the graph $G$ is a sequence $\pi=v_{1},t_{1},v_{2},t_{2},\ldots,v_{k}$ such that,

(a) $v_{1}\in{\mathcal{V}}_{\sf init}$,

(b) $v_{k}\in{\mathcal{V}}_{\sf term}$, and

(c) for each $(v_{i},t_{i},v_{i+1})$ subsequence, there exists $(v_{i},v_{i+1})\in{\mathcal{E}}$, and $t_{i}\in{\sc elab}((v_{i},v_{i+1}))$.

${\sf Paths}_{G}$ is the set of all possible paths of $G$. For a given path $\pi=v_{1},t_{1},v_{2},t_{2},\ldots,$ $v_{k}$ its trace, denoted by ${\sc vlab}(\pi)$, is the sequence ${\sc vlab}(v_{1}),t_{1},{\sc vlab}(v_{2}),t_{2},\ldots,$ ${\sc vlab}(v_{k})$. Since $G$ is a DAG, a trace of $G$ can visit the same mode finitely many times. ${\sf Trace}_{G}$ is the set of all traces of $G$.

An example transition graph for the ${\operatorname{\mathsf{Powertrain}}}$ system of Section 2.1 is shown in Figure 1. The set of vertices ${\mathcal{V}}=\{0,\ldots,4\}$ and the ${\sc vlab}$’s and ${\sc elab}$’s appear adjacent to the vertices and edges.

2.2.1 Trace containment

We will develop reasoning techniques based on reachability, abstraction, composition, and substitutivity. To this end, we will need to establish containment relations between the behaviors of systems. Here we define containment of transition graph traces. Consider transition graphs $G_{1},G_{2},$ with modes ${\mathcal{L}}_{1},{\mathcal{L}}_{2},$ and a mode map ${\sc lmap}:{\mathcal{L}}_{1}\rightarrow{\mathcal{L}}_{2}$. For a trace $\sigma=\ell_{1},t_{1},\ell_{2},t_{2},\ldots,\ell_{k}\in{\sf Trace}_{G_{1}}$, simplifying notation, we denote by ${\sc lmap}(\sigma)$ the sequence ${\sc lmap}(\ell_{1}),t_{1},{\sc lmap}(\ell_{2}),t_{2},$ $\ldots,{\sc lmap}(\ell_{k})$. We write $G_{1}\preceq_{{\sc lmap}}G_{2}$ iff for every trace $\sigma\in{\sf Trace}_{G_{1}}$, there is a trace $\sigma^{\prime}\in{\sf Trace}_{G_{2}}$ such that ${\sc lmap}(\sigma)$ is a prefix of $\sigma^{\prime}$.

Definition 2.2**.**

Given graphs $G_{1},G_{2}$ and a mode map ${\sc lmap}:{\mathcal{L}}_{1}\rightarrow{\mathcal{L}}_{2}$, a relation $R\subseteq{\mathcal{V}}_{1}\times{\mathcal{V}}_{2}$ is a forward simulation relation from $G_{1}$ to $G_{2}$ iff

1. (a)

for each $v\in{\mathcal{V}}_{1{\sf init}}$, there is $u\in{\mathcal{V}}_{2{\sf init}}$ such that $(v,u)\in R$, 2. (b)

for every $(v,u)\in R$, ${\sc lmap}({\sc vlab}_{1}(v))={\sc vlab}_{2}(u)$, and 3. (c)

for every $(v,v^{\prime})\in{\mathcal{E}}_{1}$ and $(v,u)\in R$, there exists a finite set $u_{1},\ldots,u_{k}$ such that:

(i) for each $u_{j}$, $(v,u_{j})\in R$, and

(ii) ${\sc elab}_{1}((v,v^{\prime}))\subseteq\cup_{j}{\sc elab}_{2}((u,u_{j}))$.

Proposition 2.3**.**

If there exists a forward simulation relation from $G_{1}$ to $G_{2}$ with ${\sc lmap}$ then $G_{1}\preceq_{{\sc lmap}}G_{2}$.

2.2.2 Sequential composition of graphs

We will find it convenient to define the sequential composition of two transition graphs. Intuitively, the traces of the composition of $G_{1}$ and $G_{2}$ will be those that can be obtained by concatenating a trace of $G_{1}$ with a trace of $G_{2}$. To keep the definitions and notations simple, we will assume (when taking sequential compositions) $|{\mathcal{V}}_{\sf init}|=|{\mathcal{V}}_{\sf term}|=1$; this is true of the examples we analyze. It is easy to generalize to the case when this does not hold. Under this assumption, the unique vertex in ${\mathcal{V}}_{\sf init}$ will be denoted as $v_{\sf init}$ and the unique vertex in ${\mathcal{V}}_{\sf term}$ will be denoted as $v_{\sf term}$.

Definition 2.4**.**

Given graphs $G_{1}=\langle{\mathcal{L}},{\mathcal{V}}_{1},{\mathcal{E}}_{1},{\sc vlab}_{1},{\sc elab}_{1}\rangle$ and $G_{2}=\langle{\mathcal{L}},{\mathcal{V}}_{2},{\mathcal{E}}_{2},$ ${\sc vlab}_{2},{\sc elab}_{2}\rangle$ such that ${\sc vlab}_{1}(v_{1{\sf term}})={\sc vlab}_{2}(v_{2{\sf init}})$, the sequential composition of $G_{1}$ and $G_{2}$ is the graph $G_{1}\circ G_{2}=\langle{\mathcal{L}},{\mathcal{V}},{\mathcal{E}},{\sc vlab},{\sc elab}\rangle$ where

1. (a)

${\mathcal{V}}=({\mathcal{V}}_{1}\cup{\mathcal{V}}_{2})\setminus\{v_{2{\sf init}})\}$, 2. (b)

${\mathcal{E}}={\mathcal{E}}_{1}\cup\{(v_{1{\sf term}},u)\>|\>(v_{2{\sf init}},u)\in{\mathcal{E}}_{2}\}\cup\{(v,u)\in{\mathcal{E}}_{2}\>|\>v\neq v_{2{\sf init}}\}$, 3. (c)

${\sc vlab}(v)={\sc vlab}_{1}(v)$ if $v\in{\mathcal{V}}_{1}$ and ${\sc vlab}(v)={\sc vlab}_{2}(v)$ if $v\in{\mathcal{V}}_{2}$, 4. (d)

For edge $(v,u)\in{\mathcal{E}}$, ${\sc elab}((v,u))$ equals

(i) ${\sc elab}_{1}((v,u))$, if $u\in{\mathcal{V}}_{1}$,

(ii) ${\sc elab}_{2}((v_{2{\sf init}},u))$, if $v=v_{1{\sf term}}$,

(iii) ${\sc elab}_{2}((v,u)),otherwise$.

Given our definition of trace containment between graphs, we can prove a very simple property about sequential composition.

Proposition 2.5**.**

Let $G_{1}$ and $G_{2}$ be two graphs with modes ${\mathcal{L}}$ that can be sequential composed. Then $G_{1}\preceq_{{\sf id}}G_{1}\circ G_{2}$, where ${\sf id}$ is the identity map on ${\mathcal{L}}$.

The proposition follows from the fact that every path of $G_{1}$ is a prefix of a path of $G_{1}\circ G_{2}$. Later in Section 4.1 we see examples of sequential composition.

2.3 Trajectories

The evolution of the system’s continuous state variables is formally described by continuous functions of time called trajectories. Let $n$ be the number of continuous variables in the underlying hybrid model. A trajectory for an $n$-dimensional system is a continuous function of the form $\tau:[0,T]\rightarrow{\mathbb{R}}^{n}$, where $T\geq 0$. The interval $[0,T]$ is called the domain of $\tau$ and is denoted by $\tau.{\mathit{d}om}$. The first state $\tau(0)$ is denoted by $\tau.\mathit{fstate}$, last state $\tau.\mathit{lstate}=\tau(T)$ and $\tau.\mathit{ltime}=T$. For a hybrid system with ${\mathcal{L}}$ modes, each trajectory is labeled by a mode in ${\mathcal{L}}$. A trajectory labeled by ${\mathcal{L}}$ is a pair $\langle\tau,\ell\rangle$ where $\tau$ is a trajectory and $\ell\in{\mathcal{L}}$.

A $T_{1}$-prefix of $\langle\tau,\ell\rangle$, for any $T_{1}\in\tau.{\mathit{d}om}$, is the labeled-trajectory $\langle\tau_{1},\ell\rangle$ with $\tau_{1}:[0,T_{1}]\rightarrow{\mathbb{R}}^{n}$, such that for all $t\in[0,T_{1}]$, $\tau_{1}(t)=\tau(t)$. A set of labeled-trajectories $\mathcal{T\mkern-3.0muL}$ is prefix-closed if for any $\langle\tau,\ell\rangle\in\mathcal{T\mkern-3.0muL}$, any of its prefixes are also in $\mathcal{T\mkern-3.0muL}$. A set $\mathcal{T\mkern-3.0muL}$ is deterministic if for any pair $\langle\tau_{1},\ell_{1}\rangle,\langle\tau_{2},\ell_{2}\rangle\in\mathcal{T\mkern-3.0muL}$, if $\tau_{1}.\mathit{fstate}=\tau_{2}.\mathit{fstate}$ and $\ell_{1}=\ell_{2}$ then one is a prefix of the other. A deterministic, prefix-closed set of labeled trajectories $\mathcal{T\mkern-3.0muL}$ describes the behavior of the continuous variables in modes ${\mathcal{L}}$. We denote by $\mathcal{T\mkern-3.0muL}_{\sf init,\ell}$ $=\{\tau.\mathit{fstate}\ |\ \langle\tau,\ell\rangle\in\mathcal{T\mkern-3.0muL}\}$, the set of initial states of trajectories in mode $\ell$. Without loss generality we assume that $\mathcal{T\mkern-3.0muL}_{{\sf init},\ell}$ is a connected, compact subset of ${\mathbb{R}}^{n}$. We assume that trajectories are defined for unbounded time, that is, for each $\ell\in{\mathcal{L}},T>0$, and $x\in\mathcal{T\mkern-3.0muL}_{{\sf init},\ell}$, there exists a $\langle\tau,\ell\rangle\in\mathcal{T\mkern-3.0muL}$, with $\tau.\mathit{fstate}=x$ and $\tau.\mathit{ltime}=T$.

In control theory and hybrid systems literature, the trajectories are assumed to be generated from models like ordinary differential equations (ODEs) and differential algebraic equations (DAEs). Here, we avoid an over-reliance on the models generating trajectories and closed-form expressions. Instead, DryVR works with sampled data of $\tau(\cdot)$ generated from simulations or tests.

Definition 2.6**.**

A simulator for a (deterministic and prefix-closed) set $\mathcal{T\mkern-3.0muL}$ of trajectories labeled by ${\mathcal{L}}$ is a function (or a program) ${\sc sim}$ that takes as input a mode label $\ell\in{\mathcal{L}}$, an initial state $x_{0}\in\mathcal{T\mkern-3.0muL}_{\sf init,\ell}$, and a finite sequence of time points $t_{1},\ldots,t_{k}$, and returns a sequence of states ${\sc sim}(x_{0},\ell,t_{1}),\ldots,{\sc sim}(x_{0},\ell,t_{k})$ such that there exists $\langle\tau,\ell\rangle\in\mathcal{T\mkern-3.0muL}$ with $\tau.\mathit{fstate}=x_{0}$ and for each $i\in\{1,\ldots,k\}$, ${\sc sim}(x_{0},\ell,t_{i})=\tau(t_{i})$.

The trajectories of the ${\operatorname{\mathsf{Powertrn}}}$ system are described by a Simulink® diagram. The diagram has several switch blocks and input signals that can be set appropriately to generate simulation data using the Simulink® ODE solver.

For simplicity, we assume that the simulations are perfect (as in the last equality of Definition 2.6). Formal guarantees of soundness of DryVR are not compromised if we use validated simulations instead.

Trajectory containment

Consider sets of trajectories, $\mathcal{T\mkern-3.0muL}_{1}$ labeled by ${\mathcal{L}}_{1}$ and $\mathcal{T\mkern-3.0muL}_{2}$ labeled by ${\mathcal{L}}_{2}$, and a mode map ${\sc lmap}:{\mathcal{L}}_{1}\rightarrow{\mathcal{L}}_{2}$. For a labeled trajectory $\langle\tau,\ell\rangle\in\mathcal{T\mkern-3.0muL}_{1}$, denote by ${\sc lmap}(\langle\tau,\ell\rangle)$ the labeled-trajectory $\langle\tau,{\sc lmap}(\ell)\rangle$. Write $\mathcal{T\mkern-3.0muL}_{1}\preceq_{{\sc lmap}}\mathcal{T\mkern-3.0muL}_{2}$ iff for every labeled trajectory $\langle\tau,\ell\rangle\in\mathcal{T\mkern-3.0muL}_{1}$, ${\sc lmap}(\langle\tau,\ell\rangle)\in\mathcal{T\mkern-3.0muL}_{2}$.

2.4 Hybrid systems

Definition 2.7**.**

An $n$-dimensional hybrid system ${\mathcal{H}}$ is a 4-tuple $\langle{\mathcal{L}},\Theta,G,\mathcal{T\mkern-3.0muL}\rangle$, where

(a) ${\mathcal{L}}$is a finite set of modes,

(b) $\Theta\subseteq{\mathbb{R}}^{n}$is a compact set of initial states,

(c) $G=\langle{\mathcal{L}},{\mathcal{V}},{\mathcal{E}},{\sc elab}\rangle$is a transition graph with set of modes ${\mathcal{L}}$, and

(d) $\mathcal{T\mkern-3.0muL}$is a set of deterministic, prefix-closed trajectories labeled by ${\mathcal{L}}$.

A state of the hybrid system ${\mathcal{H}}$ is a point in ${\mathbb{R}}^{n}\times{\mathcal{L}}$. The set of initial states is $\Theta\times{\mathcal{L}}_{\sf init}$. Semantics of ${\mathcal{H}}$ is given in terms of executions which are sequences of trajectories consistent with the modes defined by the transition graph. An execution of ${\mathcal{H}}$ is a sequence of labeled trajectories $\alpha=\langle\tau_{1},\ell_{1}\rangle\ldots,\langle\tau_{k-1},\ell_{k-1}\rangle,\ell_{k}$ in $\mathcal{T\mkern-3.0muL}$, such that

(a) $\tau_{1}.\mathit{fstate}\in\Theta$and $\ell_{1}\in{\mathcal{L}}_{\sf init}$,

(b) the sequence ${\sf path}({\alpha})$ defined as $\ell_{1},\tau_{1}.\mathit{ltime},\ell_{2},\ldots\ell_{k}$ is in ${\sf Trace}_{G}$, and

(c) for each consecutive trajectory, $\tau_{i+1}.\mathit{fstate}=\tau_{i}.\mathit{lstate}$.

The set of all executions of ${\mathcal{H}}$ is denoted by ${\sf Execs}_{{\mathcal{H}}}$. The first and last states of an execution $\alpha=\langle\tau_{1},\ell_{1}\rangle\ldots,\langle\tau_{k-1},\ell_{k-1}\rangle,\ell_{k}$ are $\alpha.\mathit{fstate}=\tau_{1}.\mathit{fstate}$, $\alpha.\mathit{lstate}=\tau_{k-1}.\mathit{lstate}$, and $\alpha.\mathit{fmode}=\ell_{1}$ $\alpha.\mathit{lmode}=\ell_{k}$. A state $\langle x,\ell\rangle$ is reachable at time $t$ and vertex $v$ (of graph $G$) if there exists an execution $\alpha=\langle\tau_{1},\ell_{1}\rangle\ldots,\langle\tau_{k-1},\ell_{k-1}\rangle,\ell_{k}\in{\sf Execs}_{{\mathcal{H}}}$, a path $\pi=v_{1},t_{1},\ldots v_{k}$ in ${\sf Paths}_{G}$, $i\in\{1,\ldots k\}$, and $t^{\prime}\in\tau_{i}.{\mathit{d}om}$ such that ${\sc vlab}(\pi)={\sf path}({\alpha})$, $v=v_{i}$, $\ell=\ell_{i}$, $x=\tau_{i}(t^{\prime})$, and $t=t^{\prime}+\sum_{j=1}^{i-1}t_{j}$. The set of reachable states, reach tube, and states reachable at a vertex $v$ are defined as follows.

• {\sf ReachTube}_{{\mathcal{H}}}=\{\langle x,\ell,t\rangle\>|\>\mbox{for some }v,\ \langle x,\ell\rangle\mbox{ is reachable at time t$and vertex$v}\}
• {\sf Reach}_{{\mathcal{H}}}=\{\langle x,\ell\rangle\>|\>\mbox{for some }v,t,\ \langle x,\ell\rangle\mbox{ is reachable at time t$and vertex$v}\}
• {\sf Reach}_{{\mathcal{H}}}^{v}=\{\langle x,\ell\rangle\>|\>\mbox{for some }t,\ \langle x,\ell\rangle\mbox{ is reachable at time t$and vertex$v}\}

Given a set of (unsafe) states ${\mathcal{U}}\subseteq{\mathbb{R}}^{n}\times{\mathcal{L}}$, the bounded safety verification problem is to decide whether ${\sf Reach}_{{\mathcal{H}}}\cap{\mathcal{U}}=\varnothing$. In Section 3 we will present DryVR’s algorithm for solving this decision problem.

Remark 2.8**.**

Defining paths in a graph $G$ to be maximal (i.e., end in a vertex in ${\mathcal{V}}_{{\sf term}}$) coupled with the definition above for executions in ${\mathcal{H}}$, ensures that for a vertex $v$ with outgoing edges in $G$, the execution must leave the mode ${\sc vlab}(v)$ within time bounded by the largest time in the labels of outgoing edges from $v$.

An instance of the bounded safety verification problem is defined by (a) the hybrid system for the ${\operatorname{\mathsf{Powertrn}}}$ which itself is defined by the transition graph of Figure 1 and the trajectories defined by the Simulink® model, and (b) the unsafe set (${\mathcal{U}}_{p}$): in ${\sf{powerup}}$ mode, $t>4\wedge\lambda\notin[12.4,12.6]$, in ${\sf{normal}}$ mode, $t>4\wedge\lambda\notin[14.6,14.8]$.

Containment between graphs and trajectories can be leveraged to conclude the containment of the set of reachable states of two hybrid systems.

Proposition 2.9**.**

Consider a pair of hybrid systems ${\mathcal{H}}_{i}=\langle{\mathcal{L}}_{i},\Theta_{i},G_{i},\mathcal{T\mkern-3.0muL}_{i}\rangle$, $i\in\{1,2\}$ and mode map ${\sc lmap}:{\mathcal{L}}_{1}\to{\mathcal{L}}_{2}$. If $\Theta_{1}\subseteq\Theta_{2}$, $G_{1}\preceq_{{\sc lmap}}G_{2}$, and $\mathcal{T\mkern-3.0muL}_{1}\preceq_{{\sc lmap}}\mathcal{T\mkern-3.0muL}_{2}$, then ${\sf Reach}_{{\mathcal{H}}_{1}}\subseteq{\sf Reach}_{{\mathcal{H}}_{2}}$.

2.5 ADAS and autonomous vehicle benchmarks

This is a suite of benchmarks we have created representing various common scenarios used for testing ADAS and Autonomous driving control systems. The hybrid system for a scenario is constructed by putting together several individual vehicles. The higher-level decisions (paths) followed by the vehicles are captured by transition graphs while the detailed dynamics of each vehicle comes from a black-box Simulink® simulator from Mathworks® [47].

Each vehicle has several continuous variables including the $x,y$-coordinates of the vehicle on the road, its velocity, heading, and steering angle. The vehicle can be controlled by two input signals, namely the throttle (acceleration or brake) and the steering speed. By choosing appropriate values for these input signals, we have defined the following modes for each vehicle — ${\sf{cruise}}$: move forward at constant speed, ${\sf{speedup}}$: constant acceleration, ${\sf{brake}}$: constant (slow) deceleration, ${\sf{em\_brake}}$: constant (hard) deceleration. In addition, we have designed lane switching modes ${\sf{ch\_left}}$ and ${\sf{ch\_right}}$ in which the acceleration and steering are controlled in such a manner that the vehicle switches to its left (resp. right) lane in a certain amount of time.

For each vehicle, we mainly analyze four variables: absolute position ($sx$) and velocity ($vx$) orthogonal to the road direction ($x$-axis), and absolute position ($sy$) and velocity ($vy$) along the road direction ($y$-axis). The throttle and steering are captured using the four variables. We will use subscripts to distinguish between different vehicles. The following scenarios are constructed by defining appropriate sets of initial states and transitions graphs labeled by the modes of two or more vehicles. In all of these scenarios a primary safety requirement is that the vehicles maintain safe separation. See Appendix A.1 for more details on initial states and transition graphs of each scenario.

${\operatorname{\mathsf{Merge}}}$:

Vehicle A in the left lane is behind vehicle B in the right lane. A switches through modes ${\sf{cruise}}$, ${\sf{speedup}}$, ${\sf{ch\_right}}$, and ${\sf{cruise}}$ over specified intervals to merge behind B. Variants of this scenario involve $B$ also switching to ${\sf{speedup}}$ or ${\sf{brake}}$.

${\operatorname{\mathsf{AutoPassing}}}$:

Vehicle A starts behind B in the same lane, and goes through a sequence of modes to overtake B. If B switches to ${\sf{speedup}}$ before A enters ${\sf{speedup}}$ then A aborts and changes back to right lane.

${\operatorname{\mathsf{Merge3}}}$:

Same as ${\operatorname{\mathsf{AutoPassing}}}$ with a third car C always ahead of $B$.

${\operatorname{\mathsf{AEB}}}$:

Vehicle A cruises behind B and B stops. A transits from ${\sf{cruise}}$ to ${\sf{em\_brake}}$ possibly over several different time intervals as governed by different sensors and reaction times.

3 Invariant verification

A subproblem for invariant verification is to compute ${\sf ReachTube}_{{\mathcal{H}}}$, or more specifically, the reachtubes for the set of trajectories $\mathcal{T\mkern-3.0muL}$ in a given mode, up to a time bound. This is a difficult problem, even when $\mathcal{T\mkern-3.0muL}$ is generated by white-box models. The algorithms in [17, 22, 29] approximate reachtubes using simulations and sensitivity analysis of ODE models generating $\mathcal{T\mkern-3.0muL}$. Here, we begin with a probabilistic method for estimating sensitivity from black-box simulators.

3.1 Discrepancy functions

Sensitivity of trajectories is formalized by the notion of discrepancy functions [22]. For a set $\mathcal{T\mkern-3.0muL}$, a discrepancy function is a uniformly continuous function $\beta:{\mathbb{R}}^{n}\times{\mathbb{R}}^{n}\times{{\mathbb{R}}_{\geq 0}}\rightarrow{{\mathbb{R}}_{\geq 0}}$, such that for any pair of identically labeled trajectories $\langle\tau_{1},\ell\rangle,\langle\tau_{2},\ell\rangle\in\mathcal{T\mkern-3.0muL}$, and any $t\in\tau_{1}.{\mathit{d}om}\cap\tau_{2}.{\mathit{d}om}$:

(a) $\beta$upper-bounds the distance between the trajectories, i.e.,

$\displaystyle|\tau_{1}(t)-\tau_{2}(t)|\leq\beta(\tau_{1}.\mathit{fstate},\tau_{2}.\mathit{fstate},t),$

(1) and

(b) $\beta$converges to [math] as the initial states converge, i.e., for any trajectory $\tau$ and $t\in\tau.{\mathit{d}om}$, if a sequence of trajectories $\tau_{1},\ldots,\tau_{k},\ldots$ has $\tau_{k}.\mathit{fstate}\rightarrow\tau.\mathit{fstate}$, then $\beta(\tau_{k}.\mathit{fstate},$ $\tau.\mathit{fstate},t)$ $\rightarrow 0$.

In [22] it is shown how given a $\beta$, condition (a) can used to over-approximate reachtubes from simulations, and condition (b) can be used to make these approximations arbitrarily precise. Techniques for computing $\beta$ from ODE models are developed in [29, 28, 38], but these are not applicable here in absence of such models. Instead we present a simple method for discovering discrepancy functions that only uses simulations. Our method is based on classical results on PAC learning linear separators [43]. We recall these before applying them to find discrepancy functions.

3.1.1 Learning linear separators.

For $\Gamma\subseteq{\mathbb{R}}\times{\mathbb{R}}$, a linear separator is a pair $(a,b)\in{\mathbb{R}}^{2}$ such that

[TABLE]

Let us fix a subset $\Gamma$ that has a (unknown) linear separator $(a_{*},b_{*})$. Our goal is to discover some $(a,b)$ that is a linear seprator for $\Gamma$ by sampling points in $\Gamma$ 111We prefer to present the learning question in this form as opposed to one where we learn a Boolean concept because it is closer to the task at hand.. The assumption is that elements of $\Gamma$ can be drawn according to some (unknown) distribution ${\mathcal{D}}$. With respect to ${\mathcal{D}}$, the error of a pair $(a,b)$ from satisfying Equation 2, is defined to be $\mathsf{err}_{{\mathcal{D}}}(a,b)={\mathcal{D}}(\{(x,y)\in\Gamma\>|\>x>ay+b\})$ where ${\mathcal{D}}(X)$ is the measure of set $X$ under distribution ${\mathcal{D}}$. Thus, the error is the measure of points (w.r.t. ${\mathcal{D}}$) that $(a,b)$ is not a linear separator for. There is a very simple (probabilistic) algorithm that finds a pair $(a,b)$ that is a linear separator for a large fraction of points in $\Gamma$, as follows.

Draw $k$ pairs $(x_{1},y_{1}),\ldots(x_{k},y_{k})$ from $\Gamma$ according to ${\mathcal{D}}$; the value of $k$ will be fixed later. 2. 2.

Find $(a,b)\in{\mathbb{R}}^{2}$ such that $x_{i}\leq ay_{i}+b$ for all $i\in\{1,\ldots k\}$.

Step 2 involves checking feasibility of a linear program, and so can be done efficiently. This algorithm, with high probability, finds a linear separator for a large fraction of points.

Proposition 3.1**.**

Let $\epsilon,\delta\in{{\mathbb{R}}_{+}}$. If $k\geq\frac{1}{\epsilon}\ln\frac{1}{\delta}$ then, with probability $\geq 1-\delta$, the above algorithm finds $(a,b)$ such that $\mathsf{err}_{{\mathcal{D}}}(a,b)<\epsilon$.

Proof.

The result follows from the PAC-learnability of concepts with low VC-dimension [43]. However, since the proof is very simple in this case, we reproduce it here for completeness. Let $k$ be as in the statement of the proposition, and suppose the pair $(a,b)$ identified by the algorithm has error $>\epsilon$. We will bound the probability of this happening.

Let $B=\{(x,y)\>|\>x>ay+b\}$. We know that ${\mathcal{D}}(B)>\epsilon$. The algorithm chose $(a,b)$ only because no element from $B$ was sampled in Step 1. The probability that this happens is $\leq(1-\epsilon)^{k}$. Observing that $(1-s)\leq e^{-s}$ for any $s$, we get $(1-\epsilon)^{k}\leq e^{-\epsilon k}\leq e^{-\ln\frac{1}{\delta}}=\delta$. This gives us the desired result. ∎

3.1.2 Learning discrepancy functions

Discrepancy functions will be computed from simulation data independently for each mode. Let us fix a mode $\ell\in{\mathcal{L}}$, and a domain $[0,T]$ for each trajectory. The discrepancy functions that we will learn from simulation data, will be one of two different forms, and we discuss how these are obtained.

Global exponential discrepancy (GED)

is a function of the form

[TABLE]

Here $K$ and $\gamma$ are constants. Thus, for any pair of trajectories $\tau_{1}$ and $\tau_{2}$ (for mode $\ell$), we have

[TABLE]

Taking logs on both sides and rearranging terms, we have

[TABLE]

It is easy to see that a global exponential discrepancy is nothing but a linear separator for the set $\Gamma$ consisting of pairs $(\ln\frac{|\tau_{1}(t)=\tau_{2}(t)|}{|\tau_{1}.\mathit{fstate}-\tau_{2}.\mathit{fstate}|},t)$ for all pairs of trajectories $\tau_{1},\tau_{2}$ and time $t$. Using the sampling based algorithm described before, we could construct a GED for a mode $\ell\in{\mathcal{L}}$, where sampling from $\Gamma$ reduces to using the simulator to generate traces from different states in $\mathcal{T\mkern-3.0muL}_{\sf init,\ell}$. Proposition 3.1 guarantees the correctness, with high probability, for any separator discovered by the algorithm. However, for our reachability algorithm to not be too conservative, we need $K$ and $\gamma$ to be small. Thus, when solving the linear program in Step 2 of the algorithm, we search for a solution minimizing $\gamma T+\ln K$.

Piece-wise exponential discrepancy (PED).

The second form of discrepancy functions we consider, depends upon dividing up the time domain $[0,T]$ into smaller intervals, and finding a global exponential discrepancy for each interval. Let $0=t_{0},t_{1},\ldots t_{N}=T$ be an increasing sequence of time points. Let $K,\gamma_{1},\gamma_{2},\ldots\gamma_{N}$ be such that for every pair of trajectories $\tau_{1},\tau_{2}$ (of mode $\ell$), for every $i\in\{1,\ldots,N\}$, and $t\in[t_{i-1},t_{i}]$, $|\tau_{1}(t)=\tau_{2}(t)|\leq|\tau_{1}(t_{i-1})-\tau_{2}(t_{i-1})|Ke^{\gamma_{i}t}$. Under such circumstances, the discrepancy function itself can be seen to be given as

[TABLE]

If the time points $0=t_{0},t_{1},\ldots t_{N}=T$ are fixed, then the constants $K,\gamma_{1},\gamma_{2},\ldots$ $\gamma_{N}$ can be discovered using the learning approach described for GED; here, to discover $\gamma_{i}$, we take $\Gamma_{i}$ to be the pairs obtained by restricting the trajectories to be between times $t_{i-1}$ and $t_{i}$. The sequence of time points $t_{i}$ are also dynamically constructed by our algorithm based on the following approach. Our experience suggests that a value for $\gamma$ that is $\geq 2$ results in very conservative reach tube computation. Therefore, the time points $t_{i}$ are constructed inductively to be as large as possible, while ensuring that $\gamma_{i}<2$.

3.1.3 Experiments on learning discrepancy

We used the above algorithm to learn discrepancy functions for dozens of modes with complex, nonlinear trajectories. Our experiments suggest that around 10-20 simulation traces are adequate for computing both global and piece-wise discrepancy functions. For each mode we use a set $S_{\sf train}$ of simulation traces that start from independently drawn random initial states in $\mathcal{T\mkern-3.0muL}_{\sf init,\ell}$ to learn a discrepancy function. Each trace may have $100$-$10000$ time points, depending on the relevant time horizon and sample times. Then we draw another set $S_{\sf test}$ of $1000$ simulations traces for validating the computed discrepancy. For every pair of trace in $S_{\sf test}$ and for every time point, we check whether the computed discrepancy satisfies Equation 1. We observe that for $|S_{\sf train}|>10$ the computed discrepancy function is correct for $96\%$ of the points $S_{\sf test}$ in and for $|S_{\sf train}|>20$ it is correct for more than $99.9\%$, across all experiments.

3.2 Verification algorithm

In this section, we present algorithms to solve the bounded verification problem for hybrid systems using learned exponential discrepancy functions. We first introduce an algorithm $\mathit{GraphReach}$ (Algorithm 1) which takes as input a hybrid system ${\mathcal{H}}=\langle{\mathcal{L}},\Theta,G,\mathcal{T\mkern-3.0muL}\rangle$ and returns a set of reachtubes—one for each vertex of $G$—such that their union over-approximates ${\sf ReachTube}_{{\mathcal{H}}}$.

$\mathit{GraphReach}$ maintains two data-structures:

(a) $RS$accumulates pairs of the form $\langle RT,v\rangle$, where $v\in{\mathcal{V}}$ and $RT$ is its corresponding reachtube;

(b) $\mathit{VerInit}$accumulates pairs of the form $\langle S,v\rangle$, where $v\in{\mathcal{V}}$ and $S\subset{\mathbb{R}}^{n}$ is the set of states from which the reachtube in $v$ is to be computed.

Each $v$ could be in multiple such pairs in $RS$ and $\mathit{VerInit}$. Initially, $RS=\varnothing$ and $\mathit{VerInit}=\{\langle\Theta,v_{\sf init}\rangle\}$.

$\mathit{LearnDiscrepancy(S_{\sf init},d,\ell)}$ computes the discrepancy function for mode $\ell$, from initial set $S_{\sf init}$ and upto time $d$ using the algorithm of Section 3.1. $\mathit{ReachComp}(S_{\sf init},d,\beta)$ first generates finite simulation traces from $S_{\sf init}$ and then bloats the traces to compute a reachtube using the discrepancy function $\beta$. This step is similar to the algorithm for dynamical systems given in [22].

The $\mathit{GraphReach}$ algorithm proceeds as follows: first, a topologically sorted array of the vertices of the DAG $G$ is computed in $\mathit{Order}$ (Line 1). The pointer $ptr$ iterates over the $\mathit{Order}$ and for each vertex $\mathit{curv}$ the following is computed. The variable $\mathit{dt}$ is set to the maximum transition time to other vertices from $\mathit{curv}$ (Line 1). For each possible initial set $S_{\sf init}$ corresponding to $\mathit{curv}$ in $\mathit{VerInit}$, the algorithm computes a discrepancy function (Line 1) and uses it to compute a reachtube from $S_{\sf init}$ up to time $\mathit{dt}$ (Line 1). For each successor $\mathit{nextv}$ of $\mathit{curv}$, the restriction of the computed reachtube $RT$ to the corresponding transition time interval ${\sc elab}((\mathit{curv,nextv}))$ is set as an initial set for $\mathit{nextv}$ (Lines 1–1).

The invariant verification algorithm $\mathit{VerifySafety}$ decides safety of ${\mathcal{H}}$ with respect to a given unsafe set ${\mathcal{U}}$ and uses $\mathit{GraphReach}$. The detailed pseudocode appears in Appendix A.3. This algorithm proceeds in a way similar to the simulation-based verification algorithms for dynamical and hybrid systems [22, 30]. Given initial set $\Theta$ and transition graph $G$ of ${\mathcal{H}}$, this algorithm partitions $\Theta$ into several subsets, and then for each subset $S$ it checks whether the computed over-approximate reachtube $RS$ from $S$ intersects with ${\mathcal{U}}$:

(a) If $RS$ is disjoint, the system is safe starting from $S$;

(b) if certain part of a reachtube $RT$ is contained in ${\mathcal{U}}$, the system is declared as unsafe and $RT$ with the the corresponding path of the graph are returned as counter-example witnesses;

(c) if neither of the above conditions hold, then the algorithm performs refinement to get a more precise over-approximation of $RS$.

Several refinement strategies are implemented in DryVR to accomplish the last step. Broadly, these strategies rely on splitting the initial set $S$ into smaller sets (this gives tighter discrepancy in the subsequent vertices) and splitting the edge labels of $G$ into smaller intervals (this gives smaller initial sets in the vertices).

The above description focuses on invariant properties, but the algorithm and our implementation in DryVR can verify a useful class of temporal properties. These are properties in which the time constraints only refer to the time since the last mode transition. For example, for the ${\operatorname{\mathsf{Powertrn}}}$ benchmark the tool verifies requirements like “after $4$s in ${\sf{normal}}$ mode, the air-fuel ratio should be contained in $[14.6,14.8]$ and after $4$s in ${\sf{powerup}}$ it should be in $[12.4,12.6]$”.

Correctness

Given a correct discrepancy function for each mode, we can prove the soundness and relative completeness of Algorithm 2. This analysis closely follows the proof of Theorem 19 and Theorem 21 in [20]. Combining this with the probabilistic correctness of the $\mathit{LearnDiscrepancy}$, we obtain the following probabilistic soundness guarantee.

Theorem 3.2**.**

If the $\beta$’s returned by $\mathit{LearnDiscrepancy}$ are always discrepancy functions for corresponding modes, then $\mathit{VerifySafety}({\mathcal{H}},U)$ (Algorithm 2) is sound. That is, if it outputs “SAFE”, then ${\mathcal{H}}$ is safe with respect to ${\mathcal{U}}$ and if it outputs “UNSAFE” then there exists an execution of ${\mathcal{H}}$ that enters ${\mathcal{U}}$.

3.3 Experiments on safety verification

The algorithms have been implemented in DryVR and have been used to automatically verify the benchmarks from Section 2 and an Automatic Transmission System (Appendix A.2). The transition graph, the initial set, and unsafe set are given in a text file. DryVR uses simulators for modes, and outputs either “Safe” of “Unsafe”. Reachtubes or counter-examples computed during the analysis are also stored in text files.

The implementation is in Python using the MatLab’s Python API for accessing the Simulink® simulators. Py-GLPK [31] is used to find the parameters of discrepancy functions; either global (GED) or piece-wise (PED) discrepancy can be selected by the user. Z3 [14] is used for reachtube operations. At this stage, all the benchmarks we are working on heavily rely on Mathworks® Simulink®. We don’t have a public Mathworks® license to release the tool, and it is complicated for the users to build a connection between DryVR and their own Simulink® models. We will release DryVR soon after we move the blackbox benchmarks to a different open source software.

Figure 2 shows example plots of computed safe reachtubes and counter-examples for a simplified ${\operatorname{\mathsf{AutoPassing}}}$ in which vehicle B stays in the ${\sf{cruise}}$ always. As before, vehicle A goes through a sequence of modes to overtake B. Initially, for both $i\in\{A,B\}$, $sx_{i}=vx_{i}=0$ and $vy_{i}=1$, i.e., both are cruising at constant speed at the center of the right lane; initial positions along the lane are $sy_{A}\in[0,2],sy_{B}\in[15,17]$. Figure 2(a) shows the lateral positions ($sx_{A}$ in red and $sx_{B}$ in green, in the top subplot), and the positions along the lane ($sy_{A}$ in red and $sy_{B}$ in green, in the bottom plot). Vehicle A moves to left lane ($sx$ decreases) and then back to the right, while B remains in the right lane, as A overtakes B (bottom plot). The unsafe set $(|sx_{A}-sx_{B}|<2\ \&\ |sy_{A}-sy_{B}|<2)$ is proved to be disjoint from computed reachtube. With a different initial set, $sy_{B}\in[30,40]$, DryVR finds counter-example (Figure 2(b)).

Table 1 summarizes some of the verification results obtained using DryVR. ${\operatorname{\mathsf{ATS}}}$ is an automatic transmission control system (see Appendix A.2 for more details). These experiments were performed on a laptop with Intel Core i7-6600U CPU and 16 GB RAM. The initial range of only the salient continuous variables are shown in the table. The unsafe sets are discussed with the model description. For example ${\mathcal{U}}_{c}$ means two vehicles are too close. For all the benchmarks, the algorithm terminated in a few minutes which includes the time to simulate, learn discrepancy, generate reachtubes, check the safety of the reachtube, over all refinements.

For the results presented in Table 1, we used GED. The reachtube generated by PED for ${\operatorname{\mathsf{Powertrn}}}$ is more precise, but for the rest, the reachtubes and the verification times using both GED and PED were comparable. In addition to the $\mathit{VerifySafety}$ algorithm, DryVR also looks for counter-examples by quickly generating random executions of the hybrid system. If any of these executions is found to be unsafe, DryVR will return “Unsafe” without starting the $\mathit{VerifySafety}$ algorithm.

4 Reasoning principles for trace containment

For a fixed unsafe set ${\mathcal{U}}$ and two hybrid systems ${\mathcal{H}}_{1}$ and ${\mathcal{H}}_{2}$, proving ${\sf Reach}_{{\mathcal{H}}_{1}}\subseteq{\sf Reach}_{{\mathcal{H}}_{2}}$ and the safety of ${\mathcal{H}}_{2}$, allows us to conclude the safety of ${\mathcal{H}}_{1}$. Proposition 2.9 establishes that proving containment of traces, trajectories, and initial sets of two hybrid systems, ensures the containment of their respective reach sets. These two observations together give us a method of concluding the safety of one system, from the safety of another, provided we can check trace containment of two graphs, and trajectory containment of two trajectory sets. In our examples, the set of modes ${\mathcal{L}}$ and the set of trajectories $\mathcal{T\mkern-3.0muL}$ is often the same between the hybrid systems we care about. So in this section present different reasoning principles to check trace containment between two graphs.

Semantically, a transition graph $G$ can be viewed as one-clock timed automaton, i.e., one can constructed a timed automaton $T$ with one-clock variable such that the timed traces of $T$ are exactly the traces of $G$. This observation, coupled with the fact that checking the timed language containment of one-clock timed automata [51] is decidable, allows one to conclude that checking if $G_{1}\preceq_{{\sc lmap}}G_{2}$ is decidable. However the algorithm in [51] has non-elementary complexity. Our next observation establishes that forward simulation between graphs can be checked in polynomial time. Combined with Proposition 2.3, this gives a simple sufficient condition for trace containment that can be efficiently checked.

Proposition 4.1**.**

Given graphs $G_{1}$ and $G_{2}$, and mode map ${\sc lmap}$, checking if there is a forward simulation from $G_{1}$ to $G_{2}$ is in polynomial time.

Proof.

The result can be seen to follow from the algorithm for checking timed simulations between timed automata [8] and the correspondence between one-clock timed automata; the fact that the automata have only one clock ensures that the region construction is poly-sized as opposed to exponential-sized. However, in the special case of transition graphs there is a more direct algorithm which does not involve region construction that we describe here.

Observe that if $\{R_{i}\}_{i\in I}$ is a family of forward simulations between $G_{1}$ and $G_{2}$ then $\cup_{i\in I}R_{i}$ is also a forward simulation. Thus, like classical simulations, there is a unique largest forward simulation between two graphs that is the greatest fixpoint of a functional on relations over states of the transition graph. Therefore, starting from the relation ${\mathcal{V}}_{1}\times{\mathcal{V}}_{2}$, one can progressively remove pairs $(v,u)$ such that $v$ is not simulated by $u$, until a fixpoint is reached. Moreover, in this case, since $G_{1}$ is a DAG, one can guarantee that the fixpoint will be reached in $|{\mathcal{V}}_{1}|$ iterations. ∎

Executions of hybrid systems are for bounded time, and bounded number of mode switches. This is because our transition graphs are acyclic and the labels on edges are bounded intervals. Sequential composition of graphs allows one to consider switching sequences that are longer and of a longer duration. We now present observations that will allow us to conclude the safety of a hybrid system with long switching sequences based on the safety of the system under short switching sequences. To do this we begin by observing simple properties about sequential composition of graphs. In what follows, all hybrid systems we consider will be over a fixed set of modes ${\mathcal{L}}$ and trajectory set $\mathcal{T\mkern-3.0muL}$. Also ${\sf id}$ will be identity function on ${\mathcal{L}}$. Our first observation is that trace containment is consistent with sequential composition.

Proposition 4.2**.**

Let $G_{i},G_{i}^{\prime}$, $i\in\{1,2\}$, be four transition graphs over ${\mathcal{L}}$ such that $G_{1}\circ G_{2}$ and $G_{1}^{\prime}\circ G_{2}^{\prime}$ are defined, and $G_{i}\preceq_{{\sf id}}G_{i}^{\prime}$ for $i\in\{1,2\}$. Then $G_{1}\circ G_{2}\preceq_{{\sf id}}G_{1}^{\prime}\circ G_{2}^{\prime}$.

Next we observe that sequential composition of graphs satisfies the “semi-group property”.

Proposition 4.3**.**

Let $G_{1},G_{2}$ be graphs over ${\mathcal{L}}$ for which $G_{1}\circ G_{2}$ is defined. Let $v_{1{\sf term}}$ be the unique terminal vertex of $G_{1}$. Consider the following hybrid systems: ${\mathcal{H}}=\langle{\mathcal{L}},\Theta,G_{1}\circ G_{2},\mathcal{T\mkern-3.0muL}\rangle$, ${\mathcal{H}}_{1}=\langle{\mathcal{L}},\Theta,G_{1},\mathcal{T\mkern-3.0muL}\rangle$, and {\mathcal{H}}_{2}=\langle{\mathcal{L}},{\sf Reach}_{{\mathcal{H}}_{1}}^{v_{1{\sf term}}},$$G_{2}, $\mathcal{T\mkern-3.0muL}\rangle$. Then ${\sf Reach}_{{\mathcal{H}}}={\sf Reach}_{{\mathcal{H}}_{1}}\cup{\sf Reach}_{{\mathcal{H}}_{2}}$.

Consider a graph $G$ such that $G\circ G$ is defined. Let ${\mathcal{H}}$ be the hybrid system with transition graph $G$, and ${\mathcal{H}}^{\prime}$ be the hybrid system with transition graph $G\circ G$; the modes, trajectories, and initial set for ${\mathcal{H}}$ and ${\mathcal{H}}^{\prime}$ are the same. Now by Proposition 2.5 and 2.9, we can conclude that ${\sf Reach}_{{\mathcal{H}}}\subseteq{\sf Reach}_{{\mathcal{H}}^{\prime}}$. Our main result of this section is that under some conditions, the converse also holds. This is useful because it allows us to conclude the safety of ${\mathcal{H}}^{\prime}$ from the safety of ${\mathcal{H}}$. In other words, we can conclude the safety of a hybrid system for long, possibly unbounded, switching sequences (namely ${\mathcal{H}}^{\prime}$) from the safety of the system under short switching sequences (namely ${\mathcal{H}}$).

Theorem 4.4**.**

Suppose $G$ is such that $G\circ G$ is defined. Let $v_{{\sf term}}$ be the unique terminal vertex of $G$. For natural number $i\geq 1$, define ${\mathcal{H}}_{i}=\langle{\mathcal{L}},\Theta,G^{i},\mathcal{T\mkern-3.0muL}\rangle$, where $G^{i}$ is the $i$-fold sequential composition of $G$ with itself. In particular, ${\mathcal{H}}_{1}=\langle{\mathcal{L}},\Theta,G,\mathcal{T\mkern-3.0muL}\rangle$. If ${\sf Reach}_{{\mathcal{H}}_{1}}^{v_{{\sf term}}}\subseteq\Theta$ then for all $i$, ${\sf Reach}_{{\mathcal{H}}_{i}}\subseteq{\sf Reach}_{{\mathcal{H}}_{1}}$.

Proof.

Let $\Theta_{1}={\sf Reach}_{{\mathcal{H}}_{1}}^{v_{{\sf term}}}$. From the condition in the theorem, we know that $\Theta_{1}\subseteq\Theta$. Let us define ${\mathcal{H}}_{i}^{\prime}=\langle{\mathcal{L}},\Theta_{1},G^{i},\mathcal{T\mkern-3.0muL}\rangle$. Observe that from Proposition 2.9, we have ${\sf Reach}_{{\mathcal{H}}_{i}^{\prime}}\subseteq{\sf Reach}_{{\mathcal{H}}_{i}}$.

The theorem is proved by induction on $i$. The base case (for $i=1$) trivially holds. For the induction step, assume that ${\sf Reach}_{{\mathcal{H}}_{i}}\subseteq{\sf Reach}_{{\mathcal{H}}_{1}}$. Since $\circ$ is associative, using Proposition 4.3 and the induction hypothesis, we have ${\sf Reach}_{{\mathcal{H}}_{i+1}}={\sf Reach}_{{\mathcal{H}}_{1}}\cup{\sf Reach}_{{\mathcal{H}}_{i}^{\prime}}\subseteq{\sf Reach}_{{\mathcal{H}}_{1}}\cup{\sf Reach}_{{\mathcal{H}}_{i}}={\sf Reach}_{{\mathcal{H}}_{1}}.$ ∎

Theorem 4.4 allows one to determine the set of reachable states of a set of modes ${\mathcal{L}}$ with respect to graph $G^{i}$, provided $G$ satisfies the conditions in the statement. This observation can be generalized. If a graph $G_{2}$ satisfies conditions similar to those in Theorem 4.4, then using Proposition 4.3, we can conclude that the reachable set with respect to graph $G_{1}\circ G_{2}^{i}\circ G_{3}$ is contained in the reachable set with respect to graph $G_{1}\circ G_{2}\circ G_{3}$. The formal statement of this observation and its proof is skipped in the interest of space, but we will use it in our experiments.

4.1 Experiments on trace containment reasoning

Graph simulation

Consider the ${\operatorname{\mathsf{AEB}}}$ system of Section 2.5 with the scenario where Vehicle B is stopped ahead of vehicle A, and A transits from ${\sf{cruise}}$ to ${\sf{em\_brake}}$ to avoid colliding with B. In the actual system ($G_{2}$ of Figure 3), two different sensor systems trigger the obstacle detection and emergency braking at time intervals $[1,2]$ and $[2.5,3.5]$ and take the system from vertex [math] (${\sf{cruise}}$) to two different vertices labeled with ${\sf{em\_brake}}$.

To illustrate trace containment reasoning, consider a simpler graph $G_{1}$ that allows a single transition of A from ${\sf{cruise}}$ to ${\sf{em\_brake}}$ over the interval bigger $[0.5,4.5]$. Using Proposition 2.9 and checking that graph $G_{2}\preceq_{\sf id}G_{1}$, it follows that verifying the safety of ${\operatorname{\mathsf{AEB}}}$ with $G_{1}$ is adequate to infer the safety with $G_{2}$. Figure 3(c) shows that the safe reachtubes returned by the algorithm for $G_{1}$ in red, indeed contain the reachtubes for $G_{2}$ (in blue and gray).

Sequential composition

We revisit the ${\operatorname{\mathsf{Powertrn}}}$ example of Section 2.1. The initial set $\Theta$ and unsafe set are the same as in Table 1. Let $G_{A}$ be the graph ($v_{0}$,${\sf{startup}}$) $\xrightarrow{[5,10]}$ ($v_{1}$,${\sf{normal}}$) $\xrightarrow{[10,15]}$ ($v_{2}$,${\sf{powerup}}$), and $G_{B}$ be the graph ($v_{0}$,${\sf{powerup}}$) $\xrightarrow{[5,10]}$ ($v_{1}$,${\sf{normal}}$) $\xrightarrow{[10,15]}$ ($v_{2}$,${\sf{powerup}}$). The graph $G_{1}=$ ($v_{0}$,${\sf{startup}}$) $\xrightarrow{[5,10]}$ ($v_{1}$,${\sf{normal}}$) $\xrightarrow{[10,15]}$ ($v_{2}$,${\sf{powerup}}$) $\xrightarrow{[5,10]}$ ($v_{3}$,${\sf{normal}}$) $\xrightarrow{[10,15]}$ (v_{4},$${\sf{powerup}}), can be expressed as the composition $G_{1}=G_{A}\circ G_{B}$. Consider the two hybrid systems ${\mathcal{H}}_{i}=\langle{\mathcal{L}},\Theta_{i},G_{i},\mathcal{T\mkern-3.0muL}\rangle$, $i\in\{A,B\}$ with $\Theta_{A}=\Theta$ and $\Theta_{B}={\sf Reach}_{{\mathcal{H}}_{A}}^{v_{2}}$. DryVR’s estimate of $\Theta_{B}$ had $\lambda$ in the range from $14.68$ to $14.71$. The reachset ${\sf Reach}_{{\mathcal{H}}_{B}}^{v_{2}}$ computed by DryVR had $\lambda$ from $14.69$ to $14.70$. The remaining variables also were observed to satisfy the containment condition. Therefore, ${\sf Reach}_{{\mathcal{H}}_{B}}^{v_{2}}\subseteq\Theta_{B}$. Consider the two hybrid systems ${\mathcal{H}}_{i}=\langle{\mathcal{L}},\Theta,G_{i},\mathcal{T\mkern-3.0muL}\rangle$, $i\in\{1,2\}$, where $G_{1}$ is (defined above) $G_{A}\circ G_{B}$, and $G_{2}=G_{A}\circ G_{B}\circ G_{B}\circ G_{B}$. Using Theorem 4.4 it suffices to analyze ${\mathcal{H}}_{1}$ to verify ${\mathcal{H}}_{2}$. ${\mathcal{H}}_{1}$ was been proved to be safe by DryVR without any refinement. As a sanity check, we also verified the safety of ${\mathcal{H}}_{2}$. DryVR proved ${\mathcal{H}}_{2}$ safe without any refinement as well.

5 Conclusions

The work presented in this paper takes an alternative view that complete mathematical models of hybrid systems are unavailable. Instead, the available system description combines a black-box simulator and a white-box transition graph. Starting from this point of view, we have developed the semantic framework, a probabilistic verification algorithm, and results on simulation relations and sequential composition for reasoning about complex hybrid systems over long switching sequences. Through modeling and analysis of a number of automotive control systems using implementations of the proposed approach, we hope to have demonstrated their promise. One direction for further exploration in this vein, is to consider more general timed and hybrid automata models of the white-box, and develop the necessary algorithms and the reasoning techniques.

Appendix A Appendix

A.1 ADAS and autonomous vehicle venchmarks

We provide more details for the different scenarios used for testing ADAS and Autonomous driving control systems.

Recall, that each vehicle model in Simulink® has several continuous variables including the $x,y$-coordinates of the vehicle on the road, its velocity, heading, steering angle, etc. The vehicle can be controlled by two input signals, namely the throttle (acceleration or brake) and the steering speed. By choosing appropriate values of these input signals, we have defined the following modes for each vehicle

(a) ${\sf{cruise}}$: move forward at constant speed, ${\sf{speedup}}$: constant acceleration, ${\sf{brake}}$: constant (slow) deceleration, ${\sf{em\_brake}}$: constant (hard).

We have designed lane switching modes ${\sf{ch\_left}}$ and ${\sf{ch\_right}}$ in which the acceleration and steering are controlled in such a manner that the vehicle switches to its left (resp. right) lane in a certain amount of time.

For each vehicle, we mainly analyze four variables: absolute position ($sx$) and velocity $vx$ orthogonal to the road direction ($x$-axis), and absolute position ($sy$) and velocity $vy$ along the road direction ($x$-axis). The throttle and steering information can be expressed using the four variables. We will use subscripts to distinguish between different vehicles. The following scenarios are constructed by defining appropriate sets of initial states and transitions graphs labeled by the modes of two or more vehicles.

${\operatorname{\mathsf{MergeBehind}}}$:

Initial condition: Vehicle A is in left and vehicle B is in the right lane; initial positions and speeds are in some range; A is in ${\sf{cruise}}$ mode, and B is in ${\sf{cruise}}$ or ${\sf{speedup}}$. Transition graph: Vehicle A goes through the mode sequence ${\sf{speedup}}$, ${\sf{ch\_right}}$, ${\sf{cruise}}$ with specified intervals of time to transit from mode to another mode. Requirement: A merges behind B within a time bound and maintains at least a given safe separation.

${\operatorname{\mathsf{MergeAhead}}}$:

Initial condition: Same as ${\operatorname{\mathsf{MergeBehind}}}$ with except that B is in ${\sf{cruise}}$ or ${\sf{brake}}$ mode. Transition graph: Same structure as ${\operatorname{\mathsf{MergeBehind}}}$ with different timing parameters. Requirement: A merges ahead of B and maintains at least a given safe separation.

${\operatorname{\mathsf{AutoPassing}}}$:

Initial condition: Vehicle A behind B in the same lane, with A in ${\sf{speedup}}$ and B in ${\sf{cruise}}$; initial positions and speeds are in some range. Transition graph: A goes through the mode sequence ${\sf{ch\_left}}$, ${\sf{speedup}}$, ${\sf{brake}}$, and ${\sf{ch\_right}}$, ${\sf{cruise}}$ with specified time intervals in each mode to complete the overtake maneuver. If B switches to ${\sf{speedup}}$ before A enters ${\sf{speedup}}$ then A aborts and changes back to right lane. If B switches to ${\sf{brake}}$ before A enters ${\sf{ch\_left}}$, then A should adjust the time to switch to ${\sf{ch\_left}}$ to avoid collision. Requirement: Vehicle A overtakes B while maintaining minimal safe separation.

${\operatorname{\mathsf{AEB}}}$:

(Emergency brakes) Initial condition: Vehicle A behind B in the same lane with A in ${\sf{cruise}}$, B is stopped (in ${\sf{cruise}}$ mode with velocity [math]). Initial positions and speeds are in some range; Transition graph: A transits from ${\sf{cruise}}$ to ${\sf{em\_brake}}$ over a given interval of time or several disjoint intervals of time. Requirement: Vehicle A stops behind B and maintains at least a given safe separation.

${\operatorname{\mathsf{MergeBetween}}}$:

Initial condition: Vehicle A, B, C are all in the same lane, with A behind B, B behind C, and in the ${\sf{cruise}}$ mode, initial positions and speeds are in some range. Transition graph: A goes through the mode sequence ${\sf{ch\_left}}$, ${\sf{speedup}}$, ${\sf{brake}}$, and ${\sf{ch\_right}}$, ${\sf{cruise}}$ with specified time intervals in each mode to overtake B. C transits from ${\sf{cruise}}$ to ${\sf{speedup}}$ then transits back to ${\sf{cruise}}$, so C is always ahead of A. Requirement: Vehicle A merges between B and C and any two vehicles maintain at least a given safe separation.

A.2 Automatic transmission control

We provide some details about the Automatic transmission control benchmark that we have modeled as a hybrid system that combine white-box and black-box components and we have verified using DryVR’s safety verification algorithm.

This is a slightly modified version of the Automatic Transmission model provided by Mathworks® as a Simulink® demo [46]. It is a model of an automatic transmission controller that exhibits both continuous and discrete behavior. The model has been previously used by S-taliro [26] for falsifying certain requirements. We are not aware of any verification results for this system.

For our experiments, we made some minor modifications to the Simulink® model to create the hybrid system ${\operatorname{\mathsf{ATS}}}$. This allows us to simulate the vehicle from any one of the four modes, namely, ${\sf{gear1}}$, ${\sf{gear2}}$, ${\sf{gear3}}$ and ${\sf{gear4}}$. Although the system has many variables, we are primarily interested in the car Speed ($v$), engine RPM (Erpm), impeller torque ($T_{i}$), output torque ($T_{o}$), and transmission RPM (Trpm), and therefore, use simulations that record these. Transition graph of ${\operatorname{\mathsf{ATS}}}$ encodes transition sequences and intervals for shifting from ${\sf{gear1}}$ through to ${\sf{gear4}}$. Requirement of interest is that the engine RPM is less than a specified maximum value, which in turn is important for limiting the thermal and mechanical stresses on the cylinders and camshafts. Typical unsafe set ${\mathcal{U}}_{t}$ could be Erpm $>4000$.

A.3 Safety verification algorithm

The safety verification algorithm is shown in 2. It proceeds along the line of the simulation-based verification algorithms presented in [22, 29, 23].