Paper Info
Title
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 (Vu0026V) of safety u0026 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.
Year
DOI
Venue
2019
10.1007/978-3-030-16722-6_12
FASE
Field
DocType
Citations 
Wireless network,Programming language,Software engineering,Damages,Verification and validation,Computer science,Verifiable secret sharing,Probabilistic logic,Semantics,Formal verification,Vulnerability
Conference
2
PageRank 
References 
Authors
0.37
0
2
Name
Order
Citations
PageRank
Li Huang15416.02
Eun-Young Kang221.73