Statistical Model Checking for the Analysis of Attacks in Connected Autonomous Vehicles

This paper proposes an approach for the analysis of the effects of attacks in connected autonomous vehicles by simulated attack injection and statistical model checking technique. The vehicles, together with the co-ordination algorithm among vehicles and the attacks are formalized using hybrid automata in UPPAAL framework. Then, the statistical model checker, UPPAAL-SMC, allows to study the resilience of the system to attacks across a range of circumstances and uncertainties. The approach is applied to a platoon of vehicles, and properties of the system under attack in case of various driver patterns of the platoon's leader and parameters of a data alteration attack are analyzed.