This thesis explores the simulation and characterization of cyber-attacks in autonomous connected driving systems using the UPPAAL formal modelling framework. The study focuses on vehicle platooning controlled through high-level physical simulations, representing the behavior of cyber-physical systems under normal conditions and during cyber-attacks. By leveraging Statistical Model Checking, we analyze how these systems respond when data is altered due to attacks such as Man-in-the-Middle and Spoofing.
Our findings indicate that, with high probability, the platoon remains in a safe state under specific attack scenarios, provided that certain attack parameters stay within defined thresholds. This confirms that enhanced Cooperative Adaptive Cruise Control algorithms can be effectively applied in real-world scenarios, ensuring resilience against malicious interventions. The integration of statistical model checking enhances system behavior analysis by offering formal probabilistic guarantees, leading to more informed decisions in the design and implementation phases.
Furthermore, combining high-level physical simulation with critical road surface conditions and realistic cooperative autonomous driving functionalities creates a robust framework for evaluating cyber-physical system resilience.