Car safety measures can be most effective when the cars on a street coordinate their control actions using distributed cooperative control. While each car optimizes its navigation planning locally to ensure the driver reaches his destination, all cars coordinate their actions in a distributed way in order to minimize the risk of safety hazards and collisions. These systems control the physical aspects of car movement using cyber technologies like local and remote sensor data and distributed V2V and V2I communication. They are thus cyber-physical systems. In this paper, we consider a distributed car control system that is inspired by the ambitions of the California PATH project, the CICAS system, SAFESPOT and PReVENT initiatives. We develop a formal model of a distributed car control system in which every car is controlled by adaptive cruise control. One of the major technical difficulties is that faithful models of distributed car control have both distributed systems and hybrid systems dynamics. They form distributed hybrid systems, which makes them very challenging for verification. In a formal proof system, we verify that the control model satisfies its main safety objective and guarantees collision freedom for arbitrarily many cars driving on a street even if new cars enter the lane from on-ramps or multi-lane streets. The system we present is in many ways one of the most complicated cyber-physical systems that has ever been fully verified formally.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen


    Exportieren, teilen und zitieren



    Titel :

    Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified


    Beteiligte:
    S. M. Loos (Autor:in) / A. Platzer (Autor:in) / L. Nistor (Autor:in)

    Erscheinungsdatum :

    2011


    Format / Umfang :

    30 pages


    Medientyp :

    Report


    Format :

    Keine Angabe


    Sprache :

    Englisch




    Efficiency analysis of formally verified adaptive cruise controllers

    Loos, Sarah M. / Witmer, David / Steenkiste, Peter et al. | IEEE | 2013



    Software safety architecture that can be formally verified

    Cossy,M. / STZ Softwaretechnik,DE | Kraftfahrwesen | 2004


    A Deployment Framework for Formally Verified Human-Robot Interactions

    Lestingi, Livia / Askarpour, Mehrnoosh / Bersani, Marcello M. et al. | BASE | 2021

    Freier Zugriff