Formal Verification of Safety Architectures for Automated Driving

TL;DR

This paper introduces a new formal logic framework to verify safety architectures in automated driving, enabling rigorous safety proofs and practical evaluation of safety strategies.

Contribution

It presents a novel program logic for formal verification of safety architectures, incorporating assume-guarantee reasoning and fallback mechanisms for automated driving.

Findings

Successfully formalized safety architectures for automated driving

Proved safety properties in a pull-over scenario

Experimentally evaluated the safety architecture's effectiveness

Abstract

Safety architectures play a crucial role in the safety assurance of automated driving vehicles (ADVs). They can be used as safety envelopes of black-box ADV controllers, and for graceful degradation from one ODD to another. Building on our previous work on the formalization of responsibility-sensitive safety (RSS), we introduce a novel program logic that accommodates assume-guarantee reasoning and fallback-like constructs. This allows us to formally define and prove the safety of existing and novel safety architectures. We apply the logic to a pull over scenario and experimentally evaluate the resulting safety architecture.