Formal verification of safety & security related timing constraints for a cooperative automotive system

Abstract

Modeling and analysis of timing constraints is crucial in real-time automotive systems. Modern vehicles are interconnected through wireless networks which creates vulnerabilities to external malicious attacks. Violations of cyber-security can cause safety related accidents and serious damages. To identify the potential impacts of security related threats on safety properties of interconnected automotive systems, this paper presents analysis techniques that support verification and validation (V&V) of safety & security (S/S) related timing constraints on those systems: Probabilistic extension of S/S timing constraints are specified in PrCcsl (probabilistic extension of clock constraint specification language) and the semantics of the extended constraints are translated into verifiable Uppaal models with stochastic semantics for formal verification. A set of mapping rules are proposed to facilitate the translation. An automatic translation tool, namely ProTL, is implemented based on the mapping rules. Formal verification are performed on the S/S timing constraints using Uppaal-SMC under different attack scenarios. Our approach is demonstrated on a cooperative automotive system case study.