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.
Formal Verification of Safety Architectures for Automated Driving
2023-06-04
1853640 byte
Conference paper
Electronic Resource
English
Safety verification of automated driving systems
Online Contents | 2013
|Formal Verification Method for Safety Diagnosis Software
SAE Technical Papers | 2015
|Formal verification method for safety diagnosis software
Automotive engineering | 2015
|