Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formal Modelling of Safety Architecture for Responsibility-Aware Autonomous Vehicle via Event-B Refinement

Tsutomu Kobayashi, Martin Bondu, Fuyuki Ishikawa

TL;DR

This paper tackles formal safety verification for autonomous vehicles under the GA-RSS framework, integrating a Simplex safety architecture to accommodate black-box AI controllers. It proposes a stepwise Event-B refinement strategy to tame the modelling and proof complexity across subscenarios within a pull-over case study, demonstrating how to separate safe-goal achievement from architecture and concrete manoeuvre details. Through two subscenarios (S4 and S3), the authors show how to derive invariant preconditions, design proper responses, and prove invariant preservation across controller, module, and manoeuvre levels. Although proof obligations are discharged manually due to tooling limits with real-number extensions, the work provides a practical methodology for structurally composing safety proofs in AV systems and highlights the potential for general guidelines on Event-B-based safety engineering for AVs. The approach offers a scalable pathway to validate GA-RSS in realistic scenarios and could influence formal safety assurance practices for responsibility-aware autonomous driving.

Abstract

Ensuring the safety of autonomous vehicles (AVs) is the key requisite for their acceptance in society. This complexity is the core challenge in formally proving their safety conditions with AI-based black-box controllers and surrounding objects under various traffic scenarios. This paper describes our strategy and experience in modelling, deriving, and proving the safety conditions of AVs with the Event-B refinement mechanism to reduce complexity. Our case study targets the state-of-the-art model of goal-aware responsibility-sensitive safety to argue over interactions with surrounding vehicles. We also employ the Simplex architecture to involve advanced black-box AI controllers. Our experience has demonstrated that the refinement mechanism can be effectively used to gradually develop the complex system over scenario variations.

Formal Modelling of Safety Architecture for Responsibility-Aware Autonomous Vehicle via Event-B Refinement

TL;DR

This paper tackles formal safety verification for autonomous vehicles under the GA-RSS framework, integrating a Simplex safety architecture to accommodate black-box AI controllers. It proposes a stepwise Event-B refinement strategy to tame the modelling and proof complexity across subscenarios within a pull-over case study, demonstrating how to separate safe-goal achievement from architecture and concrete manoeuvre details. Through two subscenarios (S4 and S3), the authors show how to derive invariant preconditions, design proper responses, and prove invariant preservation across controller, module, and manoeuvre levels. Although proof obligations are discharged manually due to tooling limits with real-number extensions, the work provides a practical methodology for structurally composing safety proofs in AV systems and highlights the potential for general guidelines on Event-B-based safety engineering for AVs. The approach offers a scalable pathway to validate GA-RSS in realistic scenarios and could influence formal safety assurance practices for responsibility-aware autonomous driving.

Abstract

Ensuring the safety of autonomous vehicles (AVs) is the key requisite for their acceptance in society. This complexity is the core challenge in formally proving their safety conditions with AI-based black-box controllers and surrounding objects under various traffic scenarios. This paper describes our strategy and experience in modelling, deriving, and proving the safety conditions of AVs with the Event-B refinement mechanism to reduce complexity. Our case study targets the state-of-the-art model of goal-aware responsibility-sensitive safety to argue over interactions with surrounding vehicles. We also employ the Simplex architecture to involve advanced black-box AI controllers. Our experience has demonstrated that the refinement mechanism can be effectively used to gradually develop the complex system over scenario variations.
Paper Structure (25 sections, 4 equations, 10 figures)

This paper contains 25 sections, 4 equations, 10 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Safety Architecture
  4. Responsibility-Sensitive Safety (RSS)
  5. Modelling and Proving in Event-B
  6. Event-B Model Components.
  7. Proving Consistency of Models.
  8. Example: Goal-Aware RSS for Pull Over Scenario
  9. Case Study 1: Modelling Subscenario $\mathcal{S}_4$
  10. Machine $M_{4,0}$: Whole Controller-Level Behaviour
  11. Machine $M_{4,1}$: Module-Level Behaviour
  12. Machine $M_{4,2}$: Manoeuvre-Level Behaviour
  13. Case Study 2: Modelling Subscenario $\mathcal{S}_3$
  14. Machine $M_{3,0}$: Whole Controller-Level Behaviour
  15. Machine $M_{3,1}$: Module-Level Behaviour
  16. ...and 10 more sections

Figures (10)

  • Figure 1: Component-based simplex architecture Phan2017Simplex
  • Figure 2: Structure of Event-B model components
  • Figure 3: Pull over scenario Hasuo2022GARSS
  • Figure 4: Subscenarios of pull over scenario with proper response and precondition
  • Figure 5: $M_{4,0}$: Abstract, whole controller-level machine for subscenario $\mathcal{S}_4$
  • ...and 5 more figures