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


    Future brake system architectures for automated driving

    Kunz, Armin / Liebemann, E. / Kunz, M. et al. | Springer Verlag | 2017

    Free access

    Formal Verification Method for Safety Diagnosis Software

    Narisawa, Fumio / Matsubara, Masahiro / Nishi, Masataka et al. | SAE Technical Papers | 2015


    Formal verification method for safety diagnosis software

    Narisawa,F. / Matsubara,M. / Nishi,M. et al. | Automotive engineering | 2015