Statistical Model Checking of Cooperative Autonomous Driving Systems

In automotive engineering, one of the ideas of vehicle cooperation is to improve convoy movements to increase the safety and efficiency of transportation systems. The complexity and stochastic nature of such cooperative systems pose difficulties for traditional model-checking techniques. Statistical model checking (SMC) provides an answer by using statistical inference to evaluate system features in a probabilistic way. In this work, we show how SMC offers a strong framework for assessing vehicle platooning systems in a range of operational scenarios by fusing statistical analysis and formal verification methodologies. Thanks to this approach, we managed to statistically prove a set of safety and functional properties of an autonomous vehicle platoon system.