A Preliminary Approach to Verify Platoon Behaviour Using Execution Traces and Model Checking

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.