Probabilistic verification of timing constraints in automotive systems using UPPAAL-SMC

E.-Y. Kang, D. Mu, L. Huang

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

Resumé

Modeling and analysis of non-functional properties, such as timing constraints, is crucial in automotive real-time embedded systems. East-adl is a domain specific architectural language dedicated to safety-critical automotive embedded system design. We have previously specified East-adl timing constraints in Clock Constraint Specification Language (Ccsl) and proved the correctness of specification by mapping the semantics of the constraints into Uppaal models amenable to model checking. In most cases, a bounded number of violations of timing constraints in automotive systems would not lead to system failures when the results of the violations are negligible, called Weakly-Hard (WH). Previous work is extended in this paper by including support for probabilistic analysis of timing constraints in the context of WH: Probabilistic extension of Ccsl, called PrCcsl, is defined and the East-adl timing constraints with stochastic properties are specified in PrCcsl. The semantics of the extended constraints in PrCcsl is translated into Uppaal-SMC models for formal verification. Furthermore, a set of mapping rules is proposed to facilitate guarantee of translation. Our approach is demonstrated on an autonomous traffic sign recognition vehicle case study.
OriginalsprogEngelsk
TitelIntegrated Formal Methods : 14th International Conference, IFM 2018, Maynooth, Ireland, September 5-7, 2018, Proceedings
RedaktørerCarlo A. Furia, Kirsten Winter
ForlagSpringer
Publikationsdato2018
Sider236-254
ISBN (Trykt)9783319989372
ISBN (Elektronisk)9783319989389
DOI
StatusUdgivet - 2018
Udgivet eksterntJa
Begivenhed14th International Conference - Maynooth, Irland
Varighed: 5. sep. 20187. sep. 2018

Konference

Konference14th International Conference
LandIrland
ByMaynooth
Periode05/09/201807/09/2018
NavnLecture Notes in Computer Science
Vol/bind11023
ISSN0302-9743

Fingeraftryk

Specification languages
Embedded systems
Clocks
Semantics
Traffic signs
Model checking
Real time systems
Systems analysis
Specifications
Formal verification

Citer dette

Kang, E-Y., Mu, D., & Huang, L. (2018). Probabilistic verification of timing constraints in automotive systems using UPPAAL-SMC. I C. A. Furia, & K. Winter (red.), Integrated Formal Methods: 14th International Conference, IFM 2018, Maynooth, Ireland, September 5-7, 2018, Proceedings (s. 236-254). Springer. Lecture Notes in Computer Science, Bind. 11023 https://doi.org/10.1007/978-3-319-98938-9_14
Kang, E.-Y. ; Mu, D. ; Huang, L. / Probabilistic verification of timing constraints in automotive systems using UPPAAL-SMC. Integrated Formal Methods: 14th International Conference, IFM 2018, Maynooth, Ireland, September 5-7, 2018, Proceedings. red. / Carlo A. Furia ; Kirsten Winter. Springer, 2018. s. 236-254 (Lecture Notes in Computer Science, Bind 11023).
@inproceedings{73cb3b3d5ea443baa3b8c64195dd1315,
title = "Probabilistic verification of timing constraints in automotive systems using UPPAAL-SMC",
abstract = "Modeling and analysis of non-functional properties, such as timing constraints, is crucial in automotive real-time embedded systems. East-adl is a domain specific architectural language dedicated to safety-critical automotive embedded system design. We have previously specified East-adl timing constraints in Clock Constraint Specification Language (Ccsl) and proved the correctness of specification by mapping the semantics of the constraints into Uppaal models amenable to model checking. In most cases, a bounded number of violations of timing constraints in automotive systems would not lead to system failures when the results of the violations are negligible, called Weakly-Hard (WH). Previous work is extended in this paper by including support for probabilistic analysis of timing constraints in the context of WH: Probabilistic extension of Ccsl, called PrCcsl, is defined and the East-adl timing constraints with stochastic properties are specified in PrCcsl. The semantics of the extended constraints in PrCcsl is translated into Uppaal-SMC models for formal verification. Furthermore, a set of mapping rules is proposed to facilitate guarantee of translation. Our approach is demonstrated on an autonomous traffic sign recognition vehicle case study.",
keywords = "EAST-ADL, Probabilistic CCSL, Statistical model checking, UPPAAL-SMC, Weakly-Hard System",
author = "E.-Y. Kang and D. Mu and L. Huang",
year = "2018",
doi = "10.1007/978-3-319-98938-9_14",
language = "English",
isbn = "9783319989372",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "236--254",
editor = "{A. Furia}, Carlo and Kirsten Winter",
booktitle = "Integrated Formal Methods",
address = "Germany",

}

Kang, E-Y, Mu, D & Huang, L 2018, Probabilistic verification of timing constraints in automotive systems using UPPAAL-SMC. i C A. Furia & K Winter (red), Integrated Formal Methods: 14th International Conference, IFM 2018, Maynooth, Ireland, September 5-7, 2018, Proceedings. Springer, Lecture Notes in Computer Science, bind 11023, s. 236-254, 14th International Conference, Maynooth, Irland, 05/09/2018. https://doi.org/10.1007/978-3-319-98938-9_14

Probabilistic verification of timing constraints in automotive systems using UPPAAL-SMC. / Kang, E.-Y.; Mu, D.; Huang, L.

Integrated Formal Methods: 14th International Conference, IFM 2018, Maynooth, Ireland, September 5-7, 2018, Proceedings. red. / Carlo A. Furia; Kirsten Winter. Springer, 2018. s. 236-254 (Lecture Notes in Computer Science, Bind 11023).

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

TY - GEN

T1 - Probabilistic verification of timing constraints in automotive systems using UPPAAL-SMC

AU - Kang, E.-Y.

AU - Mu, D.

AU - Huang, L.

PY - 2018

Y1 - 2018

N2 - Modeling and analysis of non-functional properties, such as timing constraints, is crucial in automotive real-time embedded systems. East-adl is a domain specific architectural language dedicated to safety-critical automotive embedded system design. We have previously specified East-adl timing constraints in Clock Constraint Specification Language (Ccsl) and proved the correctness of specification by mapping the semantics of the constraints into Uppaal models amenable to model checking. In most cases, a bounded number of violations of timing constraints in automotive systems would not lead to system failures when the results of the violations are negligible, called Weakly-Hard (WH). Previous work is extended in this paper by including support for probabilistic analysis of timing constraints in the context of WH: Probabilistic extension of Ccsl, called PrCcsl, is defined and the East-adl timing constraints with stochastic properties are specified in PrCcsl. The semantics of the extended constraints in PrCcsl is translated into Uppaal-SMC models for formal verification. Furthermore, a set of mapping rules is proposed to facilitate guarantee of translation. Our approach is demonstrated on an autonomous traffic sign recognition vehicle case study.

AB - Modeling and analysis of non-functional properties, such as timing constraints, is crucial in automotive real-time embedded systems. East-adl is a domain specific architectural language dedicated to safety-critical automotive embedded system design. We have previously specified East-adl timing constraints in Clock Constraint Specification Language (Ccsl) and proved the correctness of specification by mapping the semantics of the constraints into Uppaal models amenable to model checking. In most cases, a bounded number of violations of timing constraints in automotive systems would not lead to system failures when the results of the violations are negligible, called Weakly-Hard (WH). Previous work is extended in this paper by including support for probabilistic analysis of timing constraints in the context of WH: Probabilistic extension of Ccsl, called PrCcsl, is defined and the East-adl timing constraints with stochastic properties are specified in PrCcsl. The semantics of the extended constraints in PrCcsl is translated into Uppaal-SMC models for formal verification. Furthermore, a set of mapping rules is proposed to facilitate guarantee of translation. Our approach is demonstrated on an autonomous traffic sign recognition vehicle case study.

KW - EAST-ADL

KW - Probabilistic CCSL

KW - Statistical model checking

KW - UPPAAL-SMC

KW - Weakly-Hard System

U2 - 10.1007/978-3-319-98938-9_14

DO - 10.1007/978-3-319-98938-9_14

M3 - Article in proceedings

SN - 9783319989372

T3 - Lecture Notes in Computer Science

SP - 236

EP - 254

BT - Integrated Formal Methods

A2 - A. Furia, Carlo

A2 - Winter, Kirsten

PB - Springer

ER -

Kang E-Y, Mu D, Huang L. Probabilistic verification of timing constraints in automotive systems using UPPAAL-SMC. I A. Furia C, Winter K, red., Integrated Formal Methods: 14th International Conference, IFM 2018, Maynooth, Ireland, September 5-7, 2018, Proceedings. Springer. 2018. s. 236-254. (Lecture Notes in Computer Science, Bind 11023). https://doi.org/10.1007/978-3-319-98938-9_14