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

Research output: Contribution in Book/Catalog/Report/Conference proceedingConference contribution

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

Original languageEnglish
Title of host publicationProceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS
Pages135-144
Number of pages10
DOIs
Publication statusPublished - 15 Oct 2013
Event18th International Conference on Engineering of Complex Computer Systems, ICECCS 2013 - Singapore, Singapore
Duration: 17 Jul 201319 Jul 2013

Conference

Conference18th International Conference on Engineering of Complex Computer Systems, ICECCS 2013
CountrySingapore
CitySingapore
Period17/07/1319/07/13

Fingerprint

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

Keywords

  • EAST-ADL
  • Energy-aware Timed Embedded Systems
  • Model Checking
  • Model-Transformation

Cite this

Kang, E-Y., Perrouin, G., & Schobbens, P. Y. (2013). Model-based verification of energy-aware real-time automotive systems. In Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS (pp. 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. pp. 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. in Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS., 6601814, pp. 135-144, 18th International Conference on Engineering of Complex Computer Systems, ICECCS 2013, Singapore, Singapore, 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.

Research output: Contribution in Book/Catalog/Report/Conference proceedingConference contribution

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