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.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Formal Verification of Intersection Safety for Automated Driving


    Beteiligte:
    Haydon, James (Autor:in) / Bondu, Martin (Autor:in) / Eberhart, Clovis (Autor:in) / Dubut, Jeremy (Autor:in) / Hasuo, Ichiro (Autor:in)


    Erscheinungsdatum :

    24.09.2023


    Format / Umfang :

    687157 byte





    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch



    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. | Kraftfahrwesen | 2009


    Formal verification method for safety diagnosis software

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