In the next generation of road-based transportation systems, where vehicles exchange information and coordinate their actions, a major challenge will be to ensure that the interaction rules are safe and lead to progress. In this paper we address the problem of automatically verifying the correctness of such distributed vehicular coordination protocols. We propose a novel modeling approach for communicating mobile entities based on the concept of satisfiability modulo theories (SMT). We apply this method to an intersection collision avoidance protocol and show how the method can be used to investigate the settings under which such a protocol achieves safety and progress. Keywords: Formal verification, Vehicular coordination, SMT, Intersection collision avoidance


    Zugriff

    Download


    Exportieren, teilen und zitieren



    Titel :

    Automatically proving the correctness of vehicle coordination


    Beteiligte:
    Mikael Asplund (Autor:in)


    Erscheinungsdatum :

    2018




    Medientyp :

    Aufsatz (Zeitschrift)


    Format :

    Elektronische Ressource


    Sprache :

    Unbekannt




    Proving Correctness of Autocoded Control Software

    Alegre, Fernando / Valenzuela, Rene / Feron, Eric et al. | AIAA | 2007


    Proving Correctness of Autocoded Control Software AIAA Paper

    Alegre, F. / Valenzuela, R. / Feron, E. et al. | British Library Conference Proceedings | 2007


    Assuring the Correctness of Automatically Generated Software

    Vestal, S. / IEEE / AIAA | British Library Conference Proceedings | 1994


    Proving the Correctness of Multicopter Rotor Fault Detection and Identification Software

    Bhaumik, Ankita / Dutta, Airin / Kopsaftopoulos, Fotis et al. | IEEE | 2021