Paper ID: 2308.10365

Formal Verification of Safety Architectures for Automated Driving

Clovis Eberhart, Jérémy Dubut, James Haydon, Ichiro Hasuo

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.

Submitted: Aug 20, 2023