Statistical model checking of a dynamic vehicle platoon

Abstract In automotive engineering, vehicle platooning is a proposed method for improving convoy movements by coordinating them to increase the safety and efficiency of transportation systems. The complexity and stochastic nature of platooning systems provide difficulties for traditional model-checking techniques. However, Statistical Model Checking (SMC) offers a solution by using statistical inference to probabilistically evaluate system features. This paper shows that Uppaal SMC offers a robust framework for assessing platooning systems across various operational scenarios, combining statistical analysis and formal verification methodologies. The behaviour of the platoon is modelled stochastically to cover a wide range of driving scenarios and road surfaces. Using SMC, it has been possible to gauge the safety and functionality of the platoon by estimating the probability of several properties.