We consider an adaptive cruise control system in which control decisions are made based on position and velocity information received from other vehicles via V2V wireless communication. If the vehicles follow each other at a close distance, they have better wireless reception but collisions may occur when a follower car does not receive notice about the decelerations of the leader car fast enough to react before it is too late. If the vehicles are farther apart, they would have a bigger safety margin, but the wireless communication drops out more often, so that the follower car no longer receives what the leader car is doing. In order to guarantee safety, such a system must return control to the driver if it does not receive an update from a nearby vehicle within some timeout period. The value of this timeout parameter encodes a tradeoff between the likelihood that an update is received and the maximum safe acceleration. Combining formal verification techniques for hybrid systems with a wireless communication model, we analyze how the expected efficiency of a provably-safe adaptive cruise control system is affected by the value of this timeout.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Efficiency analysis of formally verified adaptive cruise controllers


    Contributors:


    Publication date :

    2013-10-01


    Size :

    329727 byte




    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English



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

    S. M. Loos / A. Platzer / L. Nistor | NTIS | 2011


    Software safety architecture that can be formally verified

    Cossy,M. / STZ Softwaretechnik,DE | Automotive engineering | 2004


    A Deployment Framework for Formally Verified Human-Robot Interactions

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

    Free access