ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Wed 10 Apr 2019 15:00 - 15:30 at JUPITER - Software Verification II Chair(s): Heike Wehrheim

Modeling and analysis of timing constraints is crucial in real-time automotive systems. Modern vehicles are being interconnected through vehicular wireless networks which creates vulnerability 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 the formal verification. A set of mapping patterns are proposed to facilitate the guarantee of translation. An automatic translation tool, namely ProTL, is implemented based on the mapping rules. V&V 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.

Wed 10 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change