A methodology for formal analysis and verification of EAST-ADL models

Eun-Young Kang, Eduard Paul Enoiu, Raluca Marinescu, Cristina Seceleanu, Pierre Yves Schobbens, Paul Pettersson

Résultats de recherche: Contribution à un journal/une revueArticle

Résumé

The architectural design of embedded software has a direct impact on the final implementation, with respect to performance and other quality attributes. Therefore, guaranteeing that an architectural model meets the specified requirements is beneficial for detecting software flaws early in the development process. In this paper, we present a formal modeling and verification methodology for safety-critical automotive products that are originally described in the domain-specific architectural language EAST-ADL. We propose a model-based approach that integrates the architectural models with component-aware model checking, and describe its tool support called ViTAL. The functional and timing behavior of each function block in the EAST-ADL model, as well as the interactions between function blocks are formally captured and expressed as Timed Automata models, which have precise semantics and can be formally verified with ViTAL. Furthermore, we show how our approach, supported by ViTAL, can be used to formally prove that the East-adl system model fulfills the specified real-time requirements and behavioral constraints. We demonstrate that the approach improves the modeling and verification capability of East-adl and identifies dependencies, as well as potential conflicts between different automotive functions before implementation. The method is substantiated by verifying an automotive braking system model, with respect to particular functional and timing requirements.

langue originaleAnglais
Pages (de - à)127-138
Nombre de pages12
journalReliability Engineering and System Safety
Volume120
Les DOIs
étatPublié - 31 juil. 2013

Empreinte digitale

Formal Analysis
Formal Verification
Methodology
Timing
Requirements
Model
Formal Modeling
Embedded Software
Architectural Design
Timed Automata
Tool Support
Embedded software
Architectural design
Development Process
Model checking
Model Checking
Braking
Safety
Attribute
Integrate

Citer ceci

Kang, Eun-Young ; Enoiu, Eduard Paul ; Marinescu, Raluca ; Seceleanu, Cristina ; Schobbens, Pierre Yves ; Pettersson, Paul. / A methodology for formal analysis and verification of EAST-ADL models. Dans: Reliability Engineering and System Safety. 2013 ; Vol 120. p. 127-138.
@article{900625fbc8af4371a3487a0b954a0b78,
title = "A methodology for formal analysis and verification of EAST-ADL models",
abstract = "The architectural design of embedded software has a direct impact on the final implementation, with respect to performance and other quality attributes. Therefore, guaranteeing that an architectural model meets the specified requirements is beneficial for detecting software flaws early in the development process. In this paper, we present a formal modeling and verification methodology for safety-critical automotive products that are originally described in the domain-specific architectural language EAST-ADL. We propose a model-based approach that integrates the architectural models with component-aware model checking, and describe its tool support called ViTAL. The functional and timing behavior of each function block in the EAST-ADL model, as well as the interactions between function blocks are formally captured and expressed as Timed Automata models, which have precise semantics and can be formally verified with ViTAL. Furthermore, we show how our approach, supported by ViTAL, can be used to formally prove that the East-adl system model fulfills the specified real-time requirements and behavioral constraints. We demonstrate that the approach improves the modeling and verification capability of East-adl and identifies dependencies, as well as potential conflicts between different automotive functions before implementation. The method is substantiated by verifying an automotive braking system model, with respect to particular functional and timing requirements.",
keywords = "EAST-ADL, Formal analysis, Model transformation, Model-driven development, UPPAAL PORT",
author = "Eun-Young Kang and Enoiu, {Eduard Paul} and Raluca Marinescu and Cristina Seceleanu and Schobbens, {Pierre Yves} and Paul Pettersson",
year = "2013",
month = "7",
day = "31",
doi = "10.1016/j.ress.2013.06.007",
language = "English",
volume = "120",
pages = "127--138",
journal = "Reliability Engineering and System Safety",
issn = "0951-8320",
publisher = "Elsevier Limited",

}

A methodology for formal analysis and verification of EAST-ADL models. / Kang, Eun-Young; Enoiu, Eduard Paul; Marinescu, Raluca; Seceleanu, Cristina; Schobbens, Pierre Yves; Pettersson, Paul.

Dans: Reliability Engineering and System Safety, Vol 120, 31.07.2013, p. 127-138.

Résultats de recherche: Contribution à un journal/une revueArticle

TY - JOUR

T1 - A methodology for formal analysis and verification of EAST-ADL models

AU - Kang, Eun-Young

AU - Enoiu, Eduard Paul

AU - Marinescu, Raluca

AU - Seceleanu, Cristina

AU - Schobbens, Pierre Yves

AU - Pettersson, Paul

PY - 2013/7/31

Y1 - 2013/7/31

N2 - The architectural design of embedded software has a direct impact on the final implementation, with respect to performance and other quality attributes. Therefore, guaranteeing that an architectural model meets the specified requirements is beneficial for detecting software flaws early in the development process. In this paper, we present a formal modeling and verification methodology for safety-critical automotive products that are originally described in the domain-specific architectural language EAST-ADL. We propose a model-based approach that integrates the architectural models with component-aware model checking, and describe its tool support called ViTAL. The functional and timing behavior of each function block in the EAST-ADL model, as well as the interactions between function blocks are formally captured and expressed as Timed Automata models, which have precise semantics and can be formally verified with ViTAL. Furthermore, we show how our approach, supported by ViTAL, can be used to formally prove that the East-adl system model fulfills the specified real-time requirements and behavioral constraints. We demonstrate that the approach improves the modeling and verification capability of East-adl and identifies dependencies, as well as potential conflicts between different automotive functions before implementation. The method is substantiated by verifying an automotive braking system model, with respect to particular functional and timing requirements.

AB - The architectural design of embedded software has a direct impact on the final implementation, with respect to performance and other quality attributes. Therefore, guaranteeing that an architectural model meets the specified requirements is beneficial for detecting software flaws early in the development process. In this paper, we present a formal modeling and verification methodology for safety-critical automotive products that are originally described in the domain-specific architectural language EAST-ADL. We propose a model-based approach that integrates the architectural models with component-aware model checking, and describe its tool support called ViTAL. The functional and timing behavior of each function block in the EAST-ADL model, as well as the interactions between function blocks are formally captured and expressed as Timed Automata models, which have precise semantics and can be formally verified with ViTAL. Furthermore, we show how our approach, supported by ViTAL, can be used to formally prove that the East-adl system model fulfills the specified real-time requirements and behavioral constraints. We demonstrate that the approach improves the modeling and verification capability of East-adl and identifies dependencies, as well as potential conflicts between different automotive functions before implementation. The method is substantiated by verifying an automotive braking system model, with respect to particular functional and timing requirements.

KW - EAST-ADL

KW - Formal analysis

KW - Model transformation

KW - Model-driven development

KW - UPPAAL PORT

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

U2 - 10.1016/j.ress.2013.06.007

DO - 10.1016/j.ress.2013.06.007

M3 - Article

AN - SCOPUS:84885617457

VL - 120

SP - 127

EP - 138

JO - Reliability Engineering and System Safety

JF - Reliability Engineering and System Safety

SN - 0951-8320

ER -