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

Eun-Young Kang; Gilles Perrouin; Pierre Yves Schobbens

doi:10.1109/ICECCS.2013.27

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

Eun-Young Kang, Gilles Perrouin, Pierre Yves Schobbens

Résultats de recherche: Contribution dans un livre/un catalogue/un rapport/dans les actes d'une conférence › Article 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 originale	Anglais
titre	Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS
Pages	135-144
Nombre de pages	10
Les DOIs	https://doi.org/10.1109/ICECCS.2013.27
Etat de la publication	Publié - 15 oct. 2013
Evénement	18th International Conference on Engineering of Complex Computer Systems, ICECCS 2013 - Singapore, Singapour Durée: 17 juil. 2013 → 19 juil. 2013

Une conférence

Une conférence	18th International Conference on Engineering of Complex Computer Systems, ICECCS 2013
Pays/Territoire	Singapour
La ville	Singapore
période	17/07/13 → 19/07/13

Accès au document

10.1109/ICECCS.2013.27

Autres fichiers et liens

Link to publication in Scopus

Contient cette citation

@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 = oct,

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",

note = "18th International Conference on Engineering of Complex Computer Systems, ICECCS 2013 ; Conference date: 17-07-2013 Through 19-07-2013",

}

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érence › Article 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

T2 - 18th International Conference on Engineering of Complex Computer Systems, ICECCS 2013

Y2 - 17 July 2013 through 19 July 2013

ER -

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

Résumé

Une conférence

Accès au document

Autres fichiers et liens

Empreinte digitale

Contient cette citation