Correct-by-Construction Advanced Driver Assistance Systems based on a Cognitive Architecture

TL;DR

This paper introduces a formal verification approach for advanced driver assistance systems using a cognitive architecture, enabling safe, correct-by-construction system design for complex highway driving scenarios.

Contribution

It integrates ACT-R cognitive modeling with formal methods and abstraction techniques to verify ADAS in multi-lane highway scenarios.

Findings

Successful application to multi-lane highway scenarios

Effective abstraction of continuous systems into Markov processes

Demonstrated safety and correctness in case studies

Abstract

Research into safety in autonomous and semi-autonomous vehicles has, so far, largely been focused on testing and validation through simulation. Due to the fact that failure of these autonomous systems is potentially life-endangering, formal methods arise as a complementary approach. This paper studies the application of formal methods to the verification of a human driver model built using the cognitive architecture ACT-R, and to the design of correct-by-construction Advanced Driver Assistance Systems (ADAS). The novelty lies in the integration of ACT-R in the formal analysis and an abstraction technique that enables finite representation of a large dimensional, continuous system in the form of a Markov process. The situation considered is a multi-lane highway driving scenario and the interactions that arise. The efficacy of the method is illustrated in two case studies with various driving conditions.

Equations

$$\begin{array}{rl}\Delta x& =v\cos (\psi +\rho )\Delta t,\Delta y=v\sin (\psi +\rho )\Delta t,\\ \Delta v& =a\Delta t,\Delta \psi =\frac{2v}{l}\sin (\rho )\Delta t,\end{array}$$

$$\Phi$$

$$\phi$$

$$\Delta {\rho }_h=k_{\text{far}}\Delta {\theta }_{\text{far}}+k_{\text{near}}\Delta {\theta }_{\text{near}}+k_I\min ({\theta }_{\text{near}},{\theta }_{\max })\Delta t,$$

$$\Delta a_h=k_{\text{car}}\Delta t_{\text{car}}^{\text{hw}}+k_{\text{follow}}(t_{\text{car}}^{\text{hw}}-t_{\text{follow}}^{\text{hw}})\Delta t,$$

$$P_{l_c}(t_{\text{car}}^{\text{hw}}\mid \lambda =0)=e^{-\alpha t_{\text{car}}^{\text{hw}}},$$

$$P_{l_c}(d,v\mid \lambda =1)=\frac{\log (\beta d+1)}{\log (\beta d_{\max }+1)},$$

$$P_{l_c}^{\prime }(d,v)=\sum _{i=-L}^L{P}_{l_c}(d+i,v){\int }_{d+i-\delta /2}^{d+i+\delta /2}w(z)dz.$$

$$\mathbf{P}(s,s^{\prime })=\{\begin{array}{ll}1& \text{if }{\mu }_s=1\wedge s^{\prime }=\text{Control}(s),\\ \text{textsc}DMM(s,s^{\prime })& \text{if }{\mu }_s=2,\\ 0& \text{otherwise,}\end{array}$$

$${\mathbb{P}}^{\mathcal{S}}(\phi )=\text{Pr}(s_0\models \phi ),$$

$$Act=\{{\mathrm{a}}_{\text{cl}},{\mathrm{a}}_{\text{con}},{\mathrm{a}}_{\text{dec}}\},$$

$$\mathbf{P}(s,\mathrm{a},s^{\prime })=\{\begin{array}{ll}\gamma +(1-\gamma )p& \text{if }\mathrm{a}={\mathrm{a}}_{\text{lc}}\wedge s^{\prime }=s_{\text{lc}}^{\prime },\\ (1-\gamma )(1-p)& \text{if }\mathrm{a}={\mathrm{a}}_{\text{lc}}\wedge s^{\prime }=s_{\text{con}}^{\prime },\\ \gamma & \text{if }\mathrm{a}={\mathrm{a}}_{\text{dec}}\wedge s^{\prime }=s_{\text{dec}}^{\prime },\\ (1-\gamma )p& \text{if }\mathrm{a}={\mathrm{a}}_{\text{dec}}\wedge s^{\prime }=s_{\text{lc}}^{\prime },\\ (1-\gamma )(1-p)& \text{if }\mathrm{a}={\mathrm{a}}_{\text{dec}}\wedge s^{\prime }=s_{\text{con}}^{\prime },\\ \gamma +(1-\gamma )(1-p)& \text{if }\mathrm{a}={\mathrm{a}}_{\text{con}}\wedge s^{\prime }=s_{\text{con}}^{\prime },\\ (1-\gamma )p& \text{if }\mathrm{a}={\mathrm{a}}_{\text{con}}\wedge s^{\prime }=s_{\text{lc}}^{\prime },\\ 0& \text{otherwise}\end{array}$$

$$a_{\text{ADAS}}^{\min }>a^{\min }\text{ and }{a}_{\text{ADAS}}^{\max }<a^{\max }.$$

$$a=\max (\min (a_h+a_{\text{ADAS}},a^{\max }),a^{\min }).$$

$$\mathbf{P}(s,\mathrm{a},s^{\prime })=\{\begin{array}{ll}1& \text{if }{s}^{\prime }=\text{ActControl}(s,\mathrm{a}),\\ 0& \text{otherwise,}\end{array}$$

$${\pi }^{\ast }\in {\arg \sup }_{\pi \in \Pi }{\mathbb{P}}^{\pi }(\phi )$$

$${\phi }_1=◊\text{textsc}crash,$$

$$\varphi_{2}=(\neg\textsc{crash})\>\mathcal{U}\>\big{(}(x=x_{\max})\wedge(t\leq T)\big{)},$$

Full text

I Introduction

Humans do not have a good track record on the road. Road accidents kill 1.24 million people every year and over $90\%$ of all crashes are mainly attributed to errors of human drivers [1]. While full self-driving technology is not yet available at scale, in an attempt to reduce these numbers, several car manufacturers have introduced semi-autonomous features in the form of Advanced Driver Assistance Systems (ADAS). Examples include Tesla’s Autopilot and Ford’s Co-Pilot 360. However, ensuring safety for semi-autonomous vehicles remains a major challenge with roots in the lack of coherent understanding of the human-ADAS interaction.

Existing methods to validate the safety of semi-autonomous systems rely on testing and simulation. Using real data to take statistically significant conclusions, however, is infeasible due to the time it takes to collect a sufficiently large amount of data [2]. Several approaches are based on modeling and simulating the semi-autonomous vehicle, as proposed in [3, 4, 5, 6]. Despite this, it is imperative to recognize the shortcomings of simulation in safety evaluation of complex driver assistance systems which could have life-endangering impact [7, 8].

A promising direction is to employ formal verification techniques, which are based on rigorous mathematical reasoning, to obtain strong guarantees about the ADAS, as proposed by several recent works [9, 10, 11]. In [10], Nilsson et al. synthesized a provably-correct module for adaptive cruise control from specifications given in temporal logic. However, these studies ignore the human driver behavior variability presented by a driver model, which can lead to controllers that perform poorly in corner cases. On the other hand, [11] applies model checking techniques to the verification of data-driven models of human driver behavior, yet it does not explicitly model the human cognitive process nor does it leverage this analysis as a way to bootstrap safety in the form of an ADAS.

The overarching goal of this study is to provide safety guarantees in semi-autonomous vehicles through the integration of human cognition with formal methods. As a first step in this direction, this paper focuses on giving guarantees at the design level of the ADAS. Specifically, it employs the cognitive architecture known as Adaptive Control of Thought-Rational (ACT-R): a framework for specifying computational behavioral models of human cognitive performance, embodying both the abilities (e.g. memory storage and recall, perception or motor action) and constraints (e.g. memory decay and limited motor performance) of humans [12, 13, 14, 15, 16, 17]. The work builds on the human driver model in a multi-lane highway driving scenario presented in [15]. It also expands upon [9] by applying verification techniques to an efficient abstraction of the model and extends it to allow the intervention of a provably-correct synthesized ADAS based on specifications given as temporal logic formulas.

The main contribution of this paper is threefold: first, it studies the verification of a human driver model built in a cognitive architecture through efficient model abstraction techniques. Second, it builds upon the model of human driving behavior as a way to bootstrap the desired properties in the ADAS using formal methods. Third, it introduces a flexible framework in terms of specifications which allows for different guarantees to be obtained depending on the choices made by the ADAS designer. Other contributions of this work include case studies based on specific properties and an open source implementation of the framework. To the best of our knowledge, this is the first framework that brings formal reasoning to the design of semi-autonomous vehicle solutions by taking into account the cognitive process of the human.

II Problem Formulation

We consider the driving scenario studied in [15], where a vehicle, called the ego-vehicle, is in an interaction with a lead vehicle in a multi-lane highway. We are interested in designing a correct-by-construction ADAS system for the ego-vehicle.

II-A Vehicle Model

We consider the ego-vehicle kinematics are described by

[TABLE]

where $x$ and $y$ are the coordinates of the vehicle’s center of mass, $v$ is the speed, and $\psi$ is the heading angle of the vehicle. The control inputs are steering angle $\rho$ and acceleration $a$. Finally, $l$ is the length of the vehicle, and $\Delta t$ is the time duration between two iterations of the model.

We assume that the motion of the lead vehicle is predictable. This simplifying assumption, even though not realistic in large scale, is reasonable for small road segments due to the predictability of highway driving and the possible improvements that can be introduced by using data [18].

II-B Integrated Human Driver Model in ACT-R

The ego-vehicle is driven by a human, whose behavior is represented in ACT-R. ACT-R is a framework for specifying computational behavioral models of human cognitive performance [12, 13, 14, 15, 16, 17]. It embodies two crucial cognitive aspects of humans: the abilities (e.g., memory storage, perception, and motor action) and the constraints (e.g. memory decay and limited motor performance). ACT-R can be generally described as two distinct layers: a perceptual-motor layer and a cognitive layer. The perceptual-motor layer corresponds to the interface of the cognition with the environment, being comprised of modules such as vision and motor actions. The cognitive layer is focused on memory, which can be divided into two different categories: declarative (consisting of factual knowledge and goals - e.g., “The maximum driving speed in a typical US highway is 65 mph” or “Try to get to point B”) and procedural (consisting of rules/procedures - e.g., “If the lead vehicle is going slowly, attempt an overtake”) [12].

Particularly, we focus on the model proposed by [15], which is an improved version of the model from [14] based on advances in ACT-R and real world data. It describes how a human controls a vehicle and performs an action (e.g. lane change), in the presence of other vehicles. The model, shown schematically in Fig. 2, consists of three distinct modules interacting in a sequential way:

• •

control, which manages both the lower level perception cues and the physical manipulation of the vehicle;

• •

monitoring, which maintains situational awareness through the awareness of the position of other vehicles around the ego-vehicle; and

• •

decision making, which uses the information gathered in the monitoring and control stage to determine the tactical decision to be taken (whether or not a lane change should happen).

A full description of the model and the governing equations for vehicle control generations are provided in Sec. IV.

II-C ADAS Design

We consider an ADAS that corresponds, first and foremost, to determining the possible available interventions to the system at each point in time. The actions considered must be realistic in nature; otherwise, the obtained assistance system would prove to be incompetent in a real-world scenario. Fig. 1 summarizes the interventions we consider for the ADAS, which are divided into two types: passive suggestions and active control.

In passive suggestions, it is assumed that the assistance system cannot change the decision making directly (as it is a human cognitive process), but it can influence it to a certain degree through suggestions [19]. Hence, the control inputs to the vehicle are directly provided by the human (ACT-R), i.e., $a=a_{h}$ and $\rho=\rho_{h}$, where subscript $h$ corresponds to the human, and the ADAS can only provide suggestions that can lead to safe and correct behaviors.

In active control, ADAS can have incremental control-based interventions at the level of acceleration and steering, i.e., $a=a_{h}+a_{\text{ADAS}}$ and $\rho=\rho_{h}+\rho_{\text{ADAS}}$, where the ADAS variables are constrained to ensure incremental interventions. The full details of the action availability, constraints, and intervention of the ADAS are presented in Sec. V.

II-D Specification Language

To formally express the behavioral properties of interest for the semi-autonomous system, we use Probabilistic Computation Tree Logic (PCTL) [20]. A PCTL formula combines boolean and temporal operators with probabilistic reasoning, constituting a rich specification language.

Definition 1** (PCTL Syntax).**

A PCTL formula $\Phi$ over a set of atomic propositions $AP$ can be formed according to the following grammar:

[TABLE]

where $o\in AP$ is an atomic proposition, $\wedge$ (“and”), $\vee$ (“or”), and $\neg$ (“negation”) are boolean operators, and $\bigcirc$ (“next”), $\mathcal{U}^{\leq k}$ (“bounded until”) with $k\in\mathbb{N}$, $\mathcal{U}$ (“until”), and $\Diamond$ (“eventually”) are temporal operators. $\mathbb{P}$ is the probabilistic operator, and $\sim p$ is a probability bound. The formulae $\Phi$ and $\varphi$ are called state and path formalas, respectively.

In this work, the atomic propositions represent boolean facts about the driving scenario. Through them, we can express properties of interest using PCTL, e.g., “The probability that eventually the distance to the nearest car becomes less than $d_{\text{safe}}$ is less than 0.001” can be expressed as \mathbb{P}_{<0.001}\big{(}\Diamond(\parallel\mathbf{x}-\mathbf{x}_{\text{\text{near}}}\parallel<d_{\text{safe}})\big{)}.

II-E Problem Statement

Given a vehicle, whose motion is described by (1), and a human driver represented by ACT-R, a set of initial conditions defined as a scenario $\mathcal{S}$, and a PCTL formula $\varphi$, we are interested in the following two problems:

Problem 1** (verification).**

Compute the probability that the human-vehicle system satisfies $\varphi$ in $\mathcal{S}$, i.e, $\mathbb{P}^{\mathcal{S}}(\varphi)$.

Problem 2** (synthesis).**

Design an ADAS that optimizes the probability of satisfying $\varphi$ by the human-vehicle-ADAS system in $\mathcal{S}$, i.e., $\mathbb{P}_{\bowtie}^{\mathcal{S}}(\varphi)$ with $\bowtie~{}\in~{}\{\max,\min\}$.

This is a flexible problem representation under which the specification $\varphi$ comes from the designer of the ADAS. It should be noted that the two-vehicle scenario considered in this study is non-limiting as traffic in highways tends to be sparse, allowing to reason over each of the vehicles separately as in [15]. In addition, the proposed solution to Problems 1 and 2 is general and can be easily extended to more vehicles.

III Preliminaries

In this study, we employ Markov models as the abstractions for the driving scenarios.

Definition 2** (Markov Chain (MC)).**

A MC is a tuple $\mathcal{M}=(S,\mathbf{P},s_{0},AP,\iota)$, where $S$ is a finite set of states, $\mathbf{P}:S\times S\to[0,1]$ is a transition probability function, $s_{0}\in S$ is the initial state, $AP$ is a set of atomic propositions, and $\iota:S\to 2^{AP}$ is a labelling function.

Definition 3** (Markov Decision Process (MDP)).**

An MDP is a tuple $\mathcal{M}=(S,Act,\mathbf{P},s_{0},AP,\iota)$, where $S$, $s_{0}$, $AP$, and $\iota$ are as in Definition 2, $Act$ is a finite set of actions, and $\mathbf{P}:S\times Act\times S\to[0,1]$ is a transition probability function. The set of actions available in state $s\in S$ is denoted by $Act(s)$.

Definition 4** (Path & Policy).**

A finite path of an MDP is a finite sequence of states $s_{0}s_{1}\ldots s_{n}$ such that the transition probability from $s_{i}$ to $s_{i+1}$ is non-zero under some action in $Act(s_{i})$ for all $i\in\{0,\ldots,n-1\}$. The set of all finite paths are denote by $S^{*}$. A policy for an MDP is a function $\pi:S^{*}\to Act$ that maps a finite path to an action such that $\pi(s_{0}s_{1}\ldots s_{n})\in Act(s_{n})$. The set of all policies is denoted by $\Pi$.

IV Abstraction and Verification of the Human-Vehicle System

To verify the human driver model under a specification $\varphi$, we first abstract it to a Markov Chain $\mathcal{M}_{h}$. We achieve this by discretizing the individual modules of the integrated human driver ACT-R model in [15] through the use of the vehicle model. We can then use off-the-shelf tools, e.g., PRISM [21], to perform the verification of the abstracted model. Below, for the purpose of clarify of presentation, we detail the abstraction procedure for a two-lane highway scenario, but we emphasize that the method extends trivially to $n$ lanes.

IV-A Control Module

The control module of ACT-R is fully deterministic and can be divided into lateral (i.e. steering) and longitudinal (i.e. acceleration) control. The lateral control is determined by the existence of two artifacts that the driver obtains using low-level perception cues: the near and far points. In each ACT-R cycle, the model uses perception to determine the difference in visual angles $\Delta\theta_{\text{near}}$ and $\Delta\theta_{\text{far}}$ and the difference control law for the steering angle $\rho_{h}$ is:

[TABLE]

where $k_{\text{far}}$, $k_{\text{near}}$ and $k_{I}$ are proportional control gains, and $\theta_{\max}$ is the maximum steering angle [15]. The process for the longitudinal control is similar. In each ACT-R cycle, the model starts by encoding the position of the lead vehicle and calculating the time headway to it, as well as the difference between this and the previous cycle, $\Delta t^{\text{hw}}_{\text{car}}$. The difference control law for the acceleration $a_{h}$ can then be written as:

[TABLE]

where $k_{\text{car}}$ and $k_{\text{follow}}$ are proportional gains of the control, and $t^{\text{hw}}_{\text{follow}}$ is the threshold time headway for following a vehicle [15]. To initiate a lane change, the driver begins following the near and far points of the destination lane instead of the current one [22].

The most direct approach to abstracting this module, widely seen in the literature for small scenarios (e.g. [18, 23, 24, 25]) is to represent the road as a grid with the position of the ego-vehicle being a cell in the grid. The error associated with this method of discretizing space can be reduced by decreasing the cell area, i.e., increase in resolution. However, this incurs in the problem of state explosion: as the resolution increases, the number of states in the system grows exponentially and the verification becomes intractable.

In this work, we take a different approach and focus on reducing the dimensionality of the problem into a less error-prone space. We project the human-vehicle system state $(x,y,v,\psi,a,\rho,t)\in\mathbb{R}^{7}$ to $\mathbf{x}=(x,v,\lambda,a,t)\in\mathbb{R}^{4}\times\{0,1\}$, where $x$ is bounded to a finite length of the road given by the scenario $\mathcal{S}$, and $\lambda\in\{0,1\}$ represents the index of the lane (left or right). A time discretization is induced by $\Delta t$ for all the continuous variables. Note that $t$ is included in $\mathbf{x}$ to enable the tracking of the state of the other vehicle, whose motion is assumed to be known (see Sec. II-A). We further reduce the representation by compressing the lane change maneuver into a single transition, as described below.

The evolution of the compressed model is as follows. When the vehicle is following its current lane, $\lambda$ remains the same, and $x$ and $v$ are given by (1) ($y$ is the center of lane $\lambda$ and $\psi=0$) with the control input $\Delta\rho_{h}$ being zero and $\Delta a_{h}$ given by (3). When a lane change is decided, the controls and state of the vehicle are given by (1)-(3). We declare the maneuver is complete when the vehicle has merged to the center of the final lane, updating $\lambda$. During the maneuver, we monitor the change in the truth values of the atomic propositions in addition to possible collisions. Then, we discard the maneuver trajectory and record only the two states, at which the lane-change maneuver starts and ends, and label the latter state with the propositions of the maneuver. These values can be pre-computed, stored in lookup tables, and used for deterministic transitions between the control and the next ACT-R step, producing significantly smaller models.

IV-B Decision Making and Monitoring

The decision making process to move from the right to the left lane consists of localizing the lead vehicle in the right lane and deciding whether or not to change lanes based on the time headway, $t^{\text{hw}}_{\text{car}}$. The lower this time headway, the more likely a driver is to perform the manoeuvre [26]. Let $d$ to be the distance between the two vehicles. We represent the probability of the driver performing a lane change to the left lane with an exponentially decreasing function (as in [27, 28]):

[TABLE]

where $\alpha$ is a parameter of the decision making.

A similar approach can be applied for a driver in the left lane overtaking a vehicle behind it in the right lane, except in this case the opposite effect occurs in the decision making. In such a case, the probability of changing lane can be modelled as a normalized logarithmic function over the distance between the vehicles:

[TABLE]

where $d_{\max}$ is the maximum length considered in the scenario, and $\beta$ is a parameter of the decision making. It should be noted that the values of $\alpha$ and $\beta$ could be estimated from real data for a population of drivers [27, 28].

So far, this version of decision making is not influenced by the monitoring module at all, and it relies on the measurements of the values of $t^{\text{hw}}_{\text{car}}$ and $d$ by the human. It is unrealistic to assume that the human’s measurements are perfect. In order to reflect uncertainty in these values, stochastic noise is added to the measurement of $d$ (as this is what human drivers have to instinctively measure through perception). The noise is considered to be normally distributed $w\sim\mathcal{N}(0,\sigma)$. For an integral resolution parameter, $\delta\in[0,d]$, and $L$ as the number of discrete steps for $x$, we can define:

[TABLE]

Similarly to the control module, the values of $P^{\prime}_{l_{c}}$ can be pre-computed and stored in a table to be used in stochastic transitions to the ACT-R control step of the following cycle.

IV-C Markov Chain Abstraction

We now define a finite MC $\mathcal{M}_{h}=(S,\mathbf{P},s_{0},AP,\iota)$ that unifies both modules using the discretization described above and a variable $\mu\in\{1,2\}$, where $\mu=1$ corresponds to the control step and $\mu=2$ to the decision making stage.

We define a state $s\in S$ of $\mathcal{M}_{h}$ to be a tuple $s=(\mu,x,\lambda,a,v,t)$. For a given scenario $\mathcal{S}=(\lambda_{0},x_{0},v_{0},\mathbf{x}^{ov})$, where $\mathbf{x}^{ov}$ is the state of the other vehicle, the state space $S$ is automatically generated. The transition probabilities for all $s,s^{\prime}\in S$ are given by:

[TABLE]

where Control is the lookup table for the control step described in Sec IV-A and DMM is the probability table for the decision making and monitoring stage described in Sec IV-B. The set $AP$ and labeling function $\iota$ are naturally mapped according to the tuple elements of each state $s$. It is important to note that the generated model is symbolic in nature, adding to the flexibility of the framework. Furthermore, it is worth noting that $\mathcal{M}_{h}$ captures in a one-to-one mapping all the possible outcomes of the continuous integrated driver model, under the assumptions of the distributions given by (4), (5) and (6).

IV-D Verification of the Human-Vehicle System

Given the model $\mathcal{M}_{h}$, we are interested in computing the probability of satisfying a property $\varphi$ for a given scenario $\mathcal{S}$, i.e, Problem 1. This probability is defined as:

[TABLE]

that is, the probability of $\varphi$ holding in $\mathcal{M}_{h}$ from an initial state $s_{0}$. This problem has been extensively studied in the literature [20], and many linear programming based solutions for it exist using off-the-shelf tools, e.g. PRISM [21], hence solving Problem 1.

V Synthesis Framework for the ADAS

In this section, we focus on the design of the ADAS and its representation as an MDP.

V-A Passive Suggestions

At the decision making level, the human driver model in [15] has two options: it can either change lane or continue in the current lane. These options can be influenced using suggestions (e.g. through visual or auditive cues) [19]. If a driver can be influenced to make a conscious decision to decelerate (e.g. through the suggestions of the ADAS), then there is an argument for including this action in the decision making. Thus, we consider a 3-option ADAS with the following set of action suggestions:

[TABLE]

where $\mathrm{a}_{\text{cl}}$, $\mathrm{a}_{\text{con}}$, and $\mathrm{a}_{\text{dec}}$ represent “change lane”, “continue driving in this lane”, and “decelerate” respectively. We assume that the human applies a constant deceleration value $a_{d}$ when the deceleration decision is made, i.e., $a_{h}=a_{d}$. Then, we can abstract this human-vehicle-ADAS system as an MDP in a similar fashion to the MC abstraction above. Note that the MDP includes additional states that correspond to the decision (action) of deceleration. These states can be computed using the same procedure in Sec. IV-A and the use of $a_{h}=a_{d}$. The set of actions of the MDP is $Act$.

The transition probabilities of the MDP depend on how compliant the drivers are with the suggestions. For the case that they are fully compliant, the decision making at each step can be replaced by all the possible actions in $Act$, obtaining an MDP with three deterministic transitions at this level. However, full compliancy at all times is not realistic by any means. To capture all possibilities, we define $\gamma\in[0,1]$ to be the responsiveness level of a driver to the suggestions given by the ADAS, where values 0 and 1 correspond to fully adamant and fully compliant driver, respectively. Building on the framework in [15] and Sec. IV-B, let $p$ be the probability that a driver decides to change lane at state $s$, i.e., probability of deciding to continue in the current lane is $1-p$. Furthermore, denote by $s^{\prime}_{i}$, the successor of state $s$ if the vehicle performs action $i$. Then, the transition probabilities of the MDP from the states $s\in S$ that correspond to ACT-R decision making, i.e., $\mu_{s}=2$, are given by:

[TABLE]

Note that, since $\gamma,p\in[0,1]$, the transitions are guaranteed to sum up to one under each action.

V-B Active Control

Active Acceleration Control

Active acceleration control by the ADAS is an incremental addition to the acceleration values applied by the human in the control module, i.e., $a=a_{h}+a_{\text{ADAS}}$. Let the acceleration of the vehicle bounded by $a\in[a^{\min},a^{\max}]$. In this module, a value $a_{\text{ADAS}}\in\{a_{\text{ADAS}}^{\min},\ldots,a_{\text{ADAS}}^{\max}\}$ is considered such that:

[TABLE]

Hence, the final acceleration applied to the vehicle becomes

[TABLE]

The restriction to the values of $a_{\text{ADAS}}$ presented in (8) allows the system to be incremental instead of enforcing the specific values chosen by the ADAS, i.e., it is corrective instead of assertive.

Active Steering Control

The human driver model in ACT-R uses the control law in (2) for the steering angle $\rho$ for given $k_{\text{far}},k_{\text{near}}$ and $k_{I}$ [15]. We design the active steering control of the ADAS ($\rho_{\text{ADAS}}$) to be given by the same control law with different sets of gains. Thus, actions in this part of the assistance system at the model level correspond to different sets of $\mathcal{C}_{i}=(k_{\text{far}}^{\text{ADAS}},k_{\text{near}}^{\text{ADAS}},k_{I}^{\text{ADAS}})_{i}$ available to the ADAS. The resulting steering angle applied to vehicle $\rho=\rho_{h}+\rho_{\text{ADAS}}$ essentially becomes the control law in (2), where the gains are the sum of gains for the human and ADAS, i.e., incremental (corrective) control, as exemplified in Fig. 3.

We augment the MDP obtained in Sec. V-A by adding the deterministic actions described to the control stage of the model. That is the transition probabilities of the MDP for the states $s\in S$ that correspond to ACT-R control, i.e., $\mu_{s}=1$, are given by:

[TABLE]

where ActControl is the state-action lookup table for the active control step described above.

V-C Policy Synthesis

Recall that we are interested in designing an ADAS that optimizes the probability of satisfying a given property $\varphi$ for a scenario $\mathcal{S}$, i.e, Problem 2. The finite MDP constructed by adding the actions at the decision making and control levels, $\mathcal{M}_{\text{ADAS}}$, represents all the possible choices of the ADAS at every $\Delta t$ step of the driving scenario $\mathcal{S}$. Therefore, the optimal ADAS problem is reduced to finding an optimal policy over $\mathcal{M}_{\text{ADAS}}$.

The policy that maximally satisfies $\varphi$ is defined as:

[TABLE]

and, respectively, $\arg\inf$ for minimally. The computation algorithms for such policies are well-studied in the formal synthesis literature, and there exist many off-the-shelf tools, e.g., PRISM [21], that solve this optimization problem efficiently. In addition to the optimal policy $\pi^{*}$, these tools compute the probability of satisfying $\varphi$ under $\pi^{*}$, denoted by $\mathbb{P}^{\pi^{*}}(\varphi)$.

VI Experimental Results

The proposed framework is implemented as an open source tool in Python using PRISM111Github repository: https://github.com/fgirbal/cbc_adas. To illustrate its efficacy, we performed a series of case studies using various scenarios and specifications. Due to space constraints, we can show only two of them here. We refer the reader to [29] for the full report on all the case studies.

We considered a two-lane highway scenario with both the ego-vehicle and lead vehicle driving on the right lane on a road segment that is 500 meters long ($x_{\max}=500m$). The lead vehicle is assumed to be moving at a constant speed with $\mathbf{x}^{ov}(0)=(x_{0}^{ov},v_{0}^{ov})$. The analysis below is performed based on the ACT-R parameters given in [15].

Case Study 1: We are interested in minimizing ($\bowtie=\min$) the safety property of crashing, i.e,

[TABLE]

for initial conditions given by $\mathcal{S}=(\lambda_{0},x_{0},v_{0},x_{0}^{ov},v_{0}^{ov})$. For $\mathcal{S}=(0,0m,25\frac{m}{s},50m,15\frac{m}{s})$ with no ADAS intervention, the verification framework generates $\mathbb{P}^{S}(\varphi_{1})=0.489$. In this situation, the ego-vehicle is travelling at a high speed when compared to the lead vehicle, leaving the human with little room for mistakes. The constraints imposed by the human cognitive modeling, such as memory decay, distraction and limited motor performance, inevitably lead to a high probability of crashing. By adding the ADAS to the ego-vehicle, however, this probability is reduced by more than half to $\mathbb{P}^{S,\pi^{*}}_{\min}(\varphi_{1})=0.242$, showing the effectiveness of the ADAS. Fig. 4 shows an example run for the human driver model (top), which results in a crash, and ADAS system (bottom), which avoids a crash by suggesting and actively contributing to the lane changing action early on.

Fig. 5(a) presents the variation of the probability of satisfaction of the safety specification with the change of $v_{0}$ and $v^{ov}_{0}$. As it can be observed, the introduction of the ADAS reduces the probability of crashing significantly in all the cases. Fig. 5(b) shows boxplots for the same safety property in a randomly generated sample of 100 different scenarios, obtained by uniformly sampling over bounded intervals for each of the variables. In this case, it is also observed a decrease in the probability of satisfaction of $\varphi_{1}$, with the first, second and third quartiles in Fig. 5(b) being lower for the system with the ADAS than those for the human driver alone.

Case Study 2

We are interested in maximizing ($\bowtie=\max$) the liveness property of completing the road segment in under $T$ seconds, i.e,

[TABLE]

for various sets of initial conditions given by $\mathcal{S}$.

Fig. 5(c) shows boxplots of the probability of the liveness property for $T=21s$ in a randomly generated sample of 100 different scenarios $\mathcal{S}$, obtained using the method previously described. In this situation, an increase in the probability of satisfaction of $\varphi_{2}$ is observed, with the first, second and third quartiles in Fig. 5(c) being higher for the system with the ADAS than those for the human driver alone. This again illustrates the efficacy of the ADAS in terms of the satisfaction of the liveness property, i.e., the ADAS makes the system reach the end of the road safely and faster as required by $\varphi_{2}$.

VII Final Remarks

In this work, we proposed a framework for providing guarantees in ($i$) analyses of semi-autonomous driving scenarios and ($ii$) designing ADAS through the means of formal methods and modeling of the driver’s cognitive process. We achieved this by employing ACT-R to represent the human and a novel abstraction method that enables the representation of the infinite, continuous system of human-vehicle by a finite Markov model. In the future, a data driven approach should be followed to validate the obtained results and evaluate the assumptions made about the drivers. A similar perspective can be taken for the design of the specifications, which could be learned in a closed loop fashion to minimize the difference between the full system with the ADAS and expert drivers. This is only possible due to the flexibility of the specifications allowed in the framework. Once the models are accurate according to the real world data, it is possible to deploy the obtained solutions.