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.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Formal Verification of Safety Architectures for Automated Driving


    Contributors:


    Publication date :

    2023-06-04


    Size :

    1853640 byte





    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English



    Formal Verification of Intersection Safety for Automated Driving

    Haydon, James / Bondu, Martin / Eberhart, Clovis et al. | IEEE | 2023


    Safety verification of automated driving systems

    Kianfar, Roozbeh | Online Contents | 2013


    Formal verification of layered sensing architectures

    Tyler, B / Langdon, A / Chawla, P | IEEE | 2010


    Formal Verification for Fault-Tolerant Architectures/PVS Design

    Rushby, J. / United States; National Aeronautics and Space Administration | British Library Conference Proceedings | 1995


    Testing and verification of active safety systems with coordinated automated driving

    Schoener,H.P. / Neads,S. / Schretter,N. et al. | Automotive engineering | 2009