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
04.06.2023
1853640 byte
Aufsatz (Konferenz)
Elektronische Ressource
Englisch
Safety verification of automated driving systems
Online Contents | 2013
|Formal verification of layered sensing architectures
IEEE | 2010
|Formal Verification for Fault-Tolerant Architectures/PVS Design
British Library Conference Proceedings | 1995
|Testing and verification of active safety systems with coordinated automated driving
Kraftfahrwesen | 2009
|