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

Li Huang, Eun Young Kang*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

61 Downloads (Pure)

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.

Original languageEnglish
Title of host publicationFundamental 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
EditorsReiner Hähnle, Wil van der Aalst
PublisherSpringer
Publication date2019
Pages210-227
ISBN (Print)9783030167219
ISBN (Electronic)978-3-030-16722-6
DOIs
Publication statusPublished - 2019
Event22nd 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, Czech Republic
Duration: 6. Apr 201911. Apr 2019

Conference

Conference22nd 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
Country/TerritoryCzech Republic
CityPrague
Period06/04/201911/04/2019
SeriesLecture Notes in Computer Science
Volume11424
ISSN0302-9743
SeriesTheoretical Computer Science and General Issues
Volume11424

Keywords

  • Automotive system
  • PrCcsl
  • Safety and security
  • Uppaal-SMC

Fingerprint

Dive into the research topics of 'Formal verification of safety & security related timing constraints for a cooperative automotive system'. Together they form a unique fingerprint.

Cite this