We build on our recent work on formalization of responsibility-sensitive safety (RSS) and present the first formal framework that enables mathematical proofs of the safety of control strategies in intersection scenarios. Intersection scenarios are challenging due to the complex interaction between vehicles; to cope with it, we extend the program logic dFHL in the previous work and introduce a novel formalism of hybrid control flow graphs on which our algorithm can automatically discover an RSS condition that ensures safety. An RSS condition thus discovered is experimentally evaluated; we observe that it is safe (as our safety proof says) and is not overly conservative.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Formal Verification of Intersection Safety for Automated Driving


    Contributors:


    Publication date :

    2023-09-24


    Size :

    687157 byte





    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English



    Formal Verification of Safety Architectures for Automated Driving

    Eberhart, Clovis / Dubut, Jeremy / Haydon, James et al. | IEEE | 2023


    Safety verification of automated driving systems

    Kianfar, Roozbeh | Online Contents | 2013


    Testing and verification of active safety systems with coordinated automated driving

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


    Formal verification method for safety diagnosis software

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


    Formal Verification Method for Safety Diagnosis Software

    Narisawa, Fumio / Matsubara, Masahiro / Nishi, Masataka et al. | British Library Conference Proceedings | 2015