Research Article
A Preliminary Approach to Verify Platoon Behaviour Using Execution Traces and Model Checking
@INPROCEEDINGS{10.1007/978-3-031-86370-7_25, author={Simona Correra and Valeria Sorgente and Giulia Varriano and Vittoria Nardone and Francesco Mercaldo and Antonella Santone}, title={A Preliminary Approach to Verify Platoon Behaviour Using Execution Traces and Model Checking}, proceedings={Intelligent Transport Systems. 8th International Conference, INTSYS 2024, Pisa, Italy, December 5--6, 2024, Revised Selected Papers}, proceedings_a={INTSYS}, year={2025}, month={4}, keywords={Platoon Formal Methods Autonomus Veihcle}, doi={10.1007/978-3-031-86370-7_25} }- Simona Correra
Valeria Sorgente
Giulia Varriano
Vittoria Nardone
Francesco Mercaldo
Antonella Santone
Year: 2025
A Preliminary Approach to Verify Platoon Behaviour Using Execution Traces and Model Checking
INTSYS
Springer
DOI: 10.1007/978-3-031-86370-7_25
Abstract
The rapid advancement of autonomous vehicle technology has significantly changed Intelligent Transportation Systems. Cooperative Cruise Control increases the efficiency of connected and autonomous vehicles by improving road safety, reducing fuel emissions and increasing traffic flow. By allowing vehicles to work together, Cooperative Cruise Control addresses key problems that cause road accidents, such as inadvertent braking, rear-end collisions, and driver error. This technology will enable vehicles to respond almost instantly to changes in speed and distance. Improve communication and coordination between vehicles and promote safe human distancing - reducing the chance of errors - new verification methods are needed to ensure the reliable performance of these platoon systems. This paper presents a preliminary approach to analyzing platoon system behaviors through execution traces. The aim is to develop an abstract model that reflects operations performed by platoon systems. Then, verifying the model using rigorous mathematical verification techniques,i.e.,model checking. The study ensures that the system consistently exhibits the desired behavior.
