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

Li Huang, Eun Young Kang*

*Kontaktforfatter for dette arbejde

Publikation: Bidrag til bog/antologi/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review

13 Downloads (Pure)

Resumé

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.

OriginalsprogEngelsk
TitelFundamental Approaches to Software Engineering : - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings
RedaktørerReiner Hähnle, Wil van der Aalst
ForlagSpringer
Publikationsdato2019
Sider210-227
ISBN (Trykt)9783030167219
ISBN (Elektronisk)978-3-030-16722-6
DOI
StatusUdgivet - 2019
Begivenhed22nd International Conference on Fundamental Approaches to Software Engineering, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019 - Prague, Tjekkiet
Varighed: 6. apr. 201911. apr. 2019

Konference

Konference22nd International Conference on Fundamental Approaches to Software Engineering, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019
LandTjekkiet
ByPrague
Periode06/04/201911/04/2019
NavnLecture Notes in Computer Science
Vol/bind11424
ISSN0302-9743
NavnTheoretical Computer Science and General Issues
Vol/bind11424

Fingeraftryk

Semantics
Specification languages
Clocks
Wireless networks
Accidents
Formal verification

Citer dette

Huang, L., & Kang, E. Y. (2019). Formal verification of safety & security related timing constraints for a cooperative automotive system. I R. Hähnle, & W. van der Aalst (red.), Fundamental Approaches to Software Engineering : - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings (s. 210-227). Springer. Lecture Notes in Computer Science, Bind. 11424 , Theoretical Computer Science and General Issues, Bind. 11424 https://doi.org/10.1007/978-3-030-16722-6_12
Huang, Li ; Kang, Eun Young. / Formal verification of safety & security related timing constraints for a cooperative automotive system. Fundamental Approaches to Software Engineering : - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. red. / Reiner Hähnle ; Wil van der Aalst. Springer, 2019. s. 210-227 (Lecture Notes in Computer Science, Bind 11424 ). (Theoretical Computer Science and General Issues, Bind 11424).
@inproceedings{ce262dc7942a4013a0e5f00fa8560aaf,
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 (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.",
keywords = "Automotive system, PrCcsl, Safety and security, Uppaal-SMC",
author = "Li Huang and Kang, {Eun Young}",
year = "2019",
doi = "10.1007/978-3-030-16722-6_12",
language = "English",
isbn = "9783030167219",
pages = "210--227",
editor = "Reiner H{\"a}hnle and {van der Aalst}, Wil",
booktitle = "Fundamental Approaches to Software Engineering",
publisher = "Springer",
address = "Germany",

}

Huang, L & Kang, EY 2019, Formal verification of safety & security related timing constraints for a cooperative automotive system. i R Hähnle & W van der Aalst (red), Fundamental Approaches to Software Engineering : - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. Springer, Lecture Notes in Computer Science, bind 11424 , Theoretical Computer Science and General Issues, bind 11424, s. 210-227, 22nd International Conference on Fundamental Approaches to Software Engineering, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Tjekkiet, 06/04/2019. https://doi.org/10.1007/978-3-030-16722-6_12

Formal verification of safety & security related timing constraints for a cooperative automotive system. / Huang, Li; Kang, Eun Young.

Fundamental Approaches to Software Engineering : - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. red. / Reiner Hähnle; Wil van der Aalst. Springer, 2019. s. 210-227 (Lecture Notes in Computer Science, Bind 11424 ). (Theoretical Computer Science and General Issues, Bind 11424).

Publikation: Bidrag til bog/antologi/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review

TY - GEN

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

AU - Huang, Li

AU - Kang, Eun Young

PY - 2019

Y1 - 2019

N2 - 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.

AB - 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.

KW - Automotive system

KW - PrCcsl

KW - Safety and security

KW - Uppaal-SMC

U2 - 10.1007/978-3-030-16722-6_12

DO - 10.1007/978-3-030-16722-6_12

M3 - Article in proceedings

SN - 9783030167219

SP - 210

EP - 227

BT - Fundamental Approaches to Software Engineering

A2 - Hähnle, Reiner

A2 - van der Aalst, Wil

PB - Springer

ER -

Huang L, Kang EY. Formal verification of safety & security related timing constraints for a cooperative automotive system. I Hähnle R, van der Aalst W, red., Fundamental Approaches to Software Engineering : - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. Springer. 2019. s. 210-227. (Lecture Notes in Computer Science, Bind 11424 ). (Theoretical Computer Science and General Issues, Bind 11424). https://doi.org/10.1007/978-3-030-16722-6_12