Model-based verification of energy-aware real-time automotive systems

Résultats de recherche: Contribution dans un livre/un catalogue/un rapport/dans les actes d'une conférenceArticle dans les actes d'une conférence/un colloque

Résumé

EAST-ADL is an architectural description language dedicated to safety-critical automotive embedded system design with a focus on structural specification and behavioral constraints. The current concept of EAST-ADL provides limited support for modeling and analysis of Energy-aware Real-Time (ERT) behaviors due to the absence of energy constraints modeling notations and the lack of formal semantics. We address these limitations by extending the EAST-ADL notation with energy constraints and integrating this extension with formal modeling and analysis techniques. We provide a mapping scheme as the basis for automatic model transformation between the extended EAST-ADL and priced timed automata for model checking. This methodology has been implemented in a tool called A-BeTA (Aβ) and is demonstrated by means of the Brake-By-Wire case study. Our approach enables formal modeling and verification of ERT systems in EAST-ADL and identifies potential conflicts between different automotive functions at an early stage of development

langue originaleAnglais
titreProceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS
Pages135-144
Nombre de pages10
Les DOIs
étatPublié - 15 oct. 2013
Evénement18th International Conference on Engineering of Complex Computer Systems, ICECCS 2013 - Singapore, Singapour
Durée: 17 juil. 201319 juil. 2013

Une conférence

Une conférence18th International Conference on Engineering of Complex Computer Systems, ICECCS 2013
PaysSingapour
La villeSingapore
période17/07/1319/07/13

Empreinte digitale

Model checking
Real time systems
Brakes
Embedded systems
Semantics
Systems analysis
Wire
Specifications

Citer ceci

Kang, E-Y., Perrouin, G., & Schobbens, P. Y. (2013). Model-based verification of energy-aware real-time automotive systems. Dans Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS (p. 135-144). [6601814] https://doi.org/10.1109/ICECCS.2013.27
Kang, Eun-Young ; Perrouin, Gilles ; Schobbens, Pierre Yves. / Model-based verification of energy-aware real-time automotive systems. Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS. 2013. p. 135-144
@inproceedings{84a798f932364719923e6e088aba83d8,
title = "Model-based verification of energy-aware real-time automotive systems",
abstract = "EAST-ADL is an architectural description language dedicated to safety-critical automotive embedded system design with a focus on structural specification and behavioral constraints. The current concept of EAST-ADL provides limited support for modeling and analysis of Energy-aware Real-Time (ERT) behaviors due to the absence of energy constraints modeling notations and the lack of formal semantics. We address these limitations by extending the EAST-ADL notation with energy constraints and integrating this extension with formal modeling and analysis techniques. We provide a mapping scheme as the basis for automatic model transformation between the extended EAST-ADL and priced timed automata for model checking. This methodology has been implemented in a tool called A-BeTA (Aβ) and is demonstrated by means of the Brake-By-Wire case study. Our approach enables formal modeling and verification of ERT systems in EAST-ADL and identifies potential conflicts between different automotive functions at an early stage of development",
keywords = "EAST-ADL, Energy-aware Timed Embedded Systems, Model Checking, Model-Transformation",
author = "Eun-Young Kang and Gilles Perrouin and Schobbens, {Pierre Yves}",
year = "2013",
month = "10",
day = "15",
doi = "10.1109/ICECCS.2013.27",
language = "English",
isbn = "9780769550077",
pages = "135--144",
booktitle = "Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS",

}

Kang, E-Y, Perrouin, G & Schobbens, PY 2013, Model-based verification of energy-aware real-time automotive systems. Dans Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS., 6601814, p. 135-144, 18th International Conference on Engineering of Complex Computer Systems, ICECCS 2013, Singapore, Singapour, 17/07/13. https://doi.org/10.1109/ICECCS.2013.27

Model-based verification of energy-aware real-time automotive systems. / Kang, Eun-Young; Perrouin, Gilles; Schobbens, Pierre Yves.

Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS. 2013. p. 135-144 6601814.

Résultats de recherche: Contribution dans un livre/un catalogue/un rapport/dans les actes d'une conférenceArticle dans les actes d'une conférence/un colloque

TY - GEN

T1 - Model-based verification of energy-aware real-time automotive systems

AU - Kang, Eun-Young

AU - Perrouin, Gilles

AU - Schobbens, Pierre Yves

PY - 2013/10/15

Y1 - 2013/10/15

N2 - EAST-ADL is an architectural description language dedicated to safety-critical automotive embedded system design with a focus on structural specification and behavioral constraints. The current concept of EAST-ADL provides limited support for modeling and analysis of Energy-aware Real-Time (ERT) behaviors due to the absence of energy constraints modeling notations and the lack of formal semantics. We address these limitations by extending the EAST-ADL notation with energy constraints and integrating this extension with formal modeling and analysis techniques. We provide a mapping scheme as the basis for automatic model transformation between the extended EAST-ADL and priced timed automata for model checking. This methodology has been implemented in a tool called A-BeTA (Aβ) and is demonstrated by means of the Brake-By-Wire case study. Our approach enables formal modeling and verification of ERT systems in EAST-ADL and identifies potential conflicts between different automotive functions at an early stage of development

AB - EAST-ADL is an architectural description language dedicated to safety-critical automotive embedded system design with a focus on structural specification and behavioral constraints. The current concept of EAST-ADL provides limited support for modeling and analysis of Energy-aware Real-Time (ERT) behaviors due to the absence of energy constraints modeling notations and the lack of formal semantics. We address these limitations by extending the EAST-ADL notation with energy constraints and integrating this extension with formal modeling and analysis techniques. We provide a mapping scheme as the basis for automatic model transformation between the extended EAST-ADL and priced timed automata for model checking. This methodology has been implemented in a tool called A-BeTA (Aβ) and is demonstrated by means of the Brake-By-Wire case study. Our approach enables formal modeling and verification of ERT systems in EAST-ADL and identifies potential conflicts between different automotive functions at an early stage of development

KW - EAST-ADL

KW - Energy-aware Timed Embedded Systems

KW - Model Checking

KW - Model-Transformation

UR - http://www.scopus.com/inward/record.url?scp=84885234648&partnerID=8YFLogxK

U2 - 10.1109/ICECCS.2013.27

DO - 10.1109/ICECCS.2013.27

M3 - Conference contribution

AN - SCOPUS:84885234648

SN - 9780769550077

SP - 135

EP - 144

BT - Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS

ER -

Kang E-Y, Perrouin G, Schobbens PY. Model-based verification of energy-aware real-time automotive systems. Dans Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS. 2013. p. 135-144. 6601814 https://doi.org/10.1109/ICECCS.2013.27