Table of Contents
Fetching ...

Safe by Design Autonomous Driving Systems

Marius Bozga, Joseph Sifakis

TL;DR

The paper tackles safe autonomy in driving by replacing end-to-end AI with a safe-by-design hybrid approach that decomposes driving into context-specific vistas. It models the environment with metric-graph maps and treats ADS as a dynamic system where per-vehicle autopilots operate under a Vista Manager and a Control Policy Manager, guided by three vista types (road, merging, crossing) and their two-phase control (caution and progress). Safety is established via invariants on per-vista safety and a compositional proof: if every vista type is safe and transitions are well-behaved, the whole ADS remains safe and speed-compliant, by design. The framework supports hybrid solutions for key operations like entering main roads, overtaking, and crossing intersections, and outlines future work to extend to richer maps, more maneuvers, and tighter integration with trajectory control for practical deployment.

Abstract

Developing safe autonomous driving systems is a major scientific and technical challenge. Existing AI-based end-to-end solutions do not offer the necessary safety guarantees, while traditional systems engineering approaches are defeated by the complexity of the problem. Currently, there is an increasing interest in hybrid design solutions, integrating machine learning components, when necessary, while using model-based components for goal management and planning. We study a method for building safe by design autonomous driving systems, based on the assumption that the capability to drive boils down to the coordinated execution of a given set of driving operations. The assumption is substantiated by a compositionality result considering that autopilots are dynamic systems receiving a small number of types of vistas as input, each vista defining a free space in its neighborhood. It is shown that safe driving for each type of vista in the corresponding free space, implies safe driving for any possible scenario under some easy-to-check conditions concerning the transition between vistas. The designed autopilot comprises distinct control policies one per type of vista, articulated in two consecutive phases. The first phase consists of carefully managing a potentially risky situation by virtually reducing speed, while the second phase consists of exiting the situation by accelerating. The autopilots designed use for their predictions simple functions characterizing the acceleration and deceleration capabilities of the vehicles. They cover the main driving operations, including entering a main road, overtaking, crossing intersections protected by traffic lights or signals, and driving on freeways. The results presented reinforce the case for hybrid solutions that incorporate mathematically elegant and robust decision methods that are safe by design.

Safe by Design Autonomous Driving Systems

TL;DR

The paper tackles safe autonomy in driving by replacing end-to-end AI with a safe-by-design hybrid approach that decomposes driving into context-specific vistas. It models the environment with metric-graph maps and treats ADS as a dynamic system where per-vehicle autopilots operate under a Vista Manager and a Control Policy Manager, guided by three vista types (road, merging, crossing) and their two-phase control (caution and progress). Safety is established via invariants on per-vista safety and a compositional proof: if every vista type is safe and transitions are well-behaved, the whole ADS remains safe and speed-compliant, by design. The framework supports hybrid solutions for key operations like entering main roads, overtaking, and crossing intersections, and outlines future work to extend to richer maps, more maneuvers, and tighter integration with trajectory control for practical deployment.

Abstract

Developing safe autonomous driving systems is a major scientific and technical challenge. Existing AI-based end-to-end solutions do not offer the necessary safety guarantees, while traditional systems engineering approaches are defeated by the complexity of the problem. Currently, there is an increasing interest in hybrid design solutions, integrating machine learning components, when necessary, while using model-based components for goal management and planning. We study a method for building safe by design autonomous driving systems, based on the assumption that the capability to drive boils down to the coordinated execution of a given set of driving operations. The assumption is substantiated by a compositionality result considering that autopilots are dynamic systems receiving a small number of types of vistas as input, each vista defining a free space in its neighborhood. It is shown that safe driving for each type of vista in the corresponding free space, implies safe driving for any possible scenario under some easy-to-check conditions concerning the transition between vistas. The designed autopilot comprises distinct control policies one per type of vista, articulated in two consecutive phases. The first phase consists of carefully managing a potentially risky situation by virtually reducing speed, while the second phase consists of exiting the situation by accelerating. The autopilots designed use for their predictions simple functions characterizing the acceleration and deceleration capabilities of the vehicles. They cover the main driving operations, including entering a main road, overtaking, crossing intersections protected by traffic lights or signals, and driving on freeways. The results presented reinforce the case for hybrid solutions that incorporate mathematically elegant and robust decision methods that are safe by design.
Paper Structure (26 sections, 9 theorems, 16 equations, 13 figures, 1 table)

This paper contains 26 sections, 9 theorems, 16 equations, 13 figures, 1 table.

Key Result

proposition thmcounterproposition

Let $\langle h_1, ..., h_k \rangle$ be the ordered set of speed limit signs from the front obstacles $F$ in $vs$ before $p$. The policy $\mathsf{follow}({vs,p})$ executes correctly only if In this case, the speed variation $\Delta v$ and the distance traveled $\Delta d$ satisfy, for any speed limit signal $h_i$ as above (where taking implicitly $\mathit{p}_{h_{k+1}} \stackrel{\mathit{def}}{=} p$)

Figures (13)

  • Figure 1: Vista of an ego vehicle with position $\mathit{p}_{e}$ and route $s_e$ and two arriving vehicles.
  • Figure 2: ADS as a dynamic system composed of the environment and the autopilots.
  • Figure 3: Road, merging and crossing vistas - critical sections in gray.
  • Figure 4: Architecture of the autopilot.
  • Figure 5: A vista and its characteristic parameters.
  • ...and 8 more figures

Theorems & Definitions (18)

  • proposition thmcounterproposition
  • proof
  • lemma thmcounterlemma
  • proof
  • lemma thmcounterlemma
  • proof
  • lemma thmcounterlemma
  • proof
  • lemma thmcounterlemma
  • proof
  • ...and 8 more