The aim of this study is to introduce a formal framework for analysis and synthesis of driver assistance systems. It applies formal methods to the verification of a stochastic human driver model built using the cognitive architecture ACT-R, and then bootstraps safety in semi-autonomous vehicles through the design of provably correct Advanced Driver Assistance Systems. The main contributions include the integration of probabilistic ACT-R models in the formal analysis of semi-autonomous systems and an abstraction technique that enables a finite representation of a large dimensional, continuous system in the form of a Markov model. The effectiveness of the method is illustrated in several case studies under various conditions. When it comes to driving, the numbers do not lie; more than 90% of road accidents in the US are caused by human error BID18 . In an effort to increase driver safety, some car manufacturers have introduced semi-autonomous features in the form of Advanced Driver Assistance Systems (ADAS). Despite this, guaranteeing safety in semi-autonomous vehicles remains a challenge, with most of the existing methods being based on testing and simulation BID4 BID9 BID19 BID21 , which do not provide the guarantees required for a safety critical system BID10 . Some recent works use formal verification to obtain strong guarantees about the ADAS BID5 BID13 BID15 ], yet they present engineering approaches to the problem which ignore the cognitive process of the human driver, leading to solutions that might perform poorly in corner cases.This study focuses on designing an ADAS that takes into account a stochastic model of the driver cognitive process. 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 which embodies both the abilities (e.g. memory storage or perception) and constraints (e.g. limited motor performance) of humans BID0 BID1 BID3 BID16 BID17 BID20 . The work builds on the human driver model in a multi-lane highway driving scenario presented in BID17 . It also expands upon BID5 BID12 by applying verification techniques to an efficient abstraction of the model and extends it to allow the intervention of a provably correct (up to the level of representation of the model) ADAS based on specifications given as temporal logic statements.The problem is defined as follows. Given the vehicle model from BID14 , a human driver model represented by ACT-R BID17 a set of initial conditions S, and a temporal logic formula ϕ [3], we are interested in (1) verification: computing the probability that the Human-Vehicle model satisfies ϕ in S, i.e, P S (ϕ); and (2) synthesis: designing an ADAS that optimizes the probability of satisfying ϕ by the Human-Vehicle-ADAS system in S, i.e., P S (ϕ) with ∈ {max, min}.
Verification of a human driver model based on a cognitive architecture and synthesis of a correct-by-construction ADAS from it.