Recent developments in autonomous driving, vehicle-to-vehicle communication and smart traffic controllers have provided a hope to realize platoon formation of vehicles. The main benefits of vehicle platooning include improved safety, enhanced highway utility, efficient fuel consumption and reduced highway accidents. One of the central components of reliable and efficient platoon formation is the underlying control strategies, e.g., constant spacing, variable spacing and dynamic headway. In this paper, we provide a generic formalization of platoon control strategies in higher-order logic. In particular, we formally verify the stability constraints of various strategies using the libraries of multivariate calculus and Laplace transform within the sound core of HOL Light proof assistant. We also illustrate the use of verified stability theorems to develop runtime monitors for each controller, which can be used to automatically detect the violation of stability constraints in a runtime execution or a logged trace of the platoon controller. Our proposed formalization has two main advantages: 1) it provides a framework to combine both static (theorem proving) and dynamic (runtime) verification approaches for platoon controllers, and 2) it is inline with the industrial standards, which explicitly recommend the use of formal methods for functional safety, e.g., automotive ISO 26262.


    Zugriff

    Download


    Exportieren, teilen und zitieren



    Titel :

    Formal Verification of Platoon Control Strategies


    Beteiligte:
    Rashid, Adnan (Autor:in) / Siddique, Umair (Autor:in) / Hasan, Osman (Autor:in)

    Erscheinungsdatum :

    2018


    Anmerkungen:

    15 pages, Software Engineering and Formal Methods (SEFM-2018)


    Medientyp :

    Preprint


    Format :

    Elektronische Ressource


    Sprache :

    Englisch




    Platoon Making Support and Acceptance Verification of HMI for Platoon Systems

    Kato, S. / Hashimoto, N. / Tsugawa, S. | British Library Online Contents | 2012



    Platoon control

    SAXENA APOORVA / LI HONG / GOSWAMI DIP | Europäisches Patentamt | 2019

    Freier Zugriff

    Longitudinal Platoon Control of Connected Vehicles: Analysis and Verification

    Li, Yongfu / Zhong, Zhenyu / Song, Yu et al. | IEEE | 2022


    PLATOON CONTROL

    SAXENA APOORVA / LI HONG / GOSWAMI DIP | Europäisches Patentamt | 2019

    Freier Zugriff