Formal Verification of Safety & Security Related Timing Constraints for A Cooperative Automotive System
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 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 16:00 | |||
14:00 30mTalk | DeepFault: Fault Localization For Deep Neural Networks FASE Link to publication | ||
14:30 30mTalk | Variability Abstraction and Refinement for Game-based Lifted Model Checking of full CTL FASE Aleksandar S. Dimovski Mother Teresa University, Skopje, Axel Legay INRIA Rennes, Andrzej Wąsowski IT University of Copenhagen, Denmark Link to publication | ||
15:00 30mTalk | Formal Verification of Safety & Security Related Timing Constraints for A Cooperative Automotive System FASE Link to publication | ||
15:30 30mTalk | Checking Observational Purity Of Procedures FASE Himanshu Arora , Raghavan Komondoor Indian Institute of Science, Bangalore, G. Ramalingam Microsoft Research Link to publication |