mdh.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
A Methodology for Formal Analysis and Verification of EAST-ADL Models
University of Namur, Belgium .
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. (IS (Embedded Systems))ORCID iD: 0000-0003-2416-4205
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. (IS (Embedded Systems))ORCID iD: 0000-0002-7663-5497
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. (IS (Embedded Systems))ORCID iD: 0000-0003-2870-2680
Show others and affiliations
2013 (English)In: Reliability Engineering & System Safety, ISSN 0951-8320, E-ISSN 1879-0836, Vol. 120, no Special Issue, 127-138 p.Article in journal (Refereed) Published
Abstract [en]

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.

Place, publisher, year, edition, pages
Elsevier , 2013. Vol. 120, no Special Issue, 127-138 p.
Keyword [en]
EAST-ADL, UPPAAL PORT, Formal Analysis, Model-driven Development, Model transformation
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:mdh:diva-21308DOI: 10.1016/j.ress.2013.06.007ISI: 000324974000016Scopus ID: 2-s2.0-84885617457OAI: oai:DiVA.org:mdh-21308DiVA: diva2:650384
Projects
ATAC - Advanced Test Automation for Complex Software-Intensive System (ITEA2/Vinnova)MBAT - Combined Model-based Analysis and Testing (Artemis/Vinnova)
Available from: 2013-09-20 Created: 2013-09-11 Last updated: 2016-08-17Bibliographically approved
In thesis
1. Model-checking and Model-based Testing of Automotive Embedded Systems: Starting from the System Architecture
Open this publication in new window or tab >>Model-checking and Model-based Testing of Automotive Embedded Systems: Starting from the System Architecture
2014 (English)Licentiate thesis, comprehensive summary (Other academic)
Abstract [en]

Nowadays, modern vehicles are equipped with electrical and electronic systems that implement highly complex functions such as anti-lock braking or cruise control. The use of such embedded systems in the automotive domain requires a revised development process that addresses their particular features. In this context, architectural models have been introduced in system development as convenient abstractions of the system’s structure represented as interacting components. To enjoy the full benefits of such abstractions, the architectural models should be complemented by an analysis framework that provides means for formal verification, and ideally also model-based testing, tailored to complex automotive systems. One major difficulty in developing such a framework lies in the fact that architectural models represent the system’s structure as well as inter-component communication, often without the actual description of the behavior. This entails the need to integrate the two “views” (structural and behavioral) in order to integrate them in a formal framework for verification.

In this thesis, we propose an integrated formal modeling and analysis methodology for automotive embedded systems that are originally described in the domain-specific architectural language EAST-ADL. Our analysis methodology relies on formal veri- fication of the original EAST-ADL model by model-checking with UPPAAL PORT for component-based analysis, and UPPAAL SMC for statistical model-checking. To enable this, we first propose a formal description of the EAST-ADL components as networks of timed automata (TA), which are UPPAAL’s modeling language. Since C code implementation is in fact what is deployed on the vehicle, it is highly desirable to narrow the gap between the code and the architectural model, but also to test the implementation for various requirements. To accomplish the former, we define an exe- cutable semantics of the UPPAAL PORT components. To be able to support testing of EAST-ADL based implementations, we take advantage of the model-checker’s ability to generate witness traces during verification of reachability properties. Consequently, we employ UPPAAL PORT to generate such traces that become our abstract test-cases. By pairing the automated model-based test-case generator with an automatic transformation from the abstract test-cases to Python scripts, we enable the execution of the generated 

Python scripts (our concrete test cases) on the system under test. The entire formal analysis and model-based testing framework is one solution to analyzing EAST-ADL models by model-checking techniques We show the framework’s applicability on an automotive industrial prototype, namely a Brake-by-Wire system. 

Place, publisher, year, edition, pages
Västerås: Mälardalen University, 2014
Series
Mälardalen University Press Licentiate Theses, ISSN 1651-9256 ; 188
National Category
Embedded Systems
Research subject
Computer Science
Identifiers
urn:nbn:se:mdh:diva-26501 (URN)978-91-7485-177-9 (ISBN)
Presentation
2014-12-19, Gamma, Mälardalens högskola, Västerås, 13:15 (English)
Opponent
Supervisors
Available from: 2014-11-10 Created: 2014-11-09 Last updated: 2014-12-12Bibliographically approved
2. Model-driven Analysis and Verification of Automotive Embedded Systems
Open this publication in new window or tab >>Model-driven Analysis and Verification of Automotive Embedded Systems
2016 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

Modern vehicles are equipped with electrical and electronic systems that implement highly complex functions, such as anti-lock braking, cruise control, etc. To realize and integrate such complex embedded systems, the automotive development process requires an updated methodology that takes into consideration the system’s intricate features and examines both their functional and extra-functional requirements. Early design artifacts like architectural models represent convenient abstractions for reasoning about the system’s structure and functionality. In this context, the EAST-ADL language has been developed as a domain-specific architectural language that targets the automotive industry and is aligned with the AUTOSAR automotive standard. To fully enjoy the benefits of these abstract system descriptions, architectural models need to be integrated into a model-driven development framework that enables also verification by, e.g., model checking and model-based testing. One major drawback in developing such a framework lies in the fact that architectural models, while capturing the system’s structure and inter-component communication, often lack direct means to represent the desired internal behavior of the system in a semantically well-defined way. To overcome this, one needs to provide means of integrating both structural as well as behavioral information, desirably within the same framework backed by formal semantics, in order to enable the model’s formal verification.

In this thesis, we propose a tool-supported integrated formal modeling and verification framework tailored for automotive embedded systems that are originally described in the EAST-ADL architectural language. To achieve this, we first provide formal semantics to the architectural model and its behavior by proposing an equivalent formal description as a network of timed automata. This enables us to analyze the resulting network of timed automata formally by model checking, using both the UPPAAL PORT and UPPAAL SMC model checkers. UPPAAL PORT is providing efficient component-aware verification via the partial order reduction technique, while UPPAAL SMC is extending UPPAAL with statistical model-checking capabilities via probabilistic algorithms. We focus the analysis on functional and timing requirements, but also on the system’s resource usage with respect to different resources specified in the model, such as memory and energy. In an attempt to narrow the gap between the original architectural model and the eventual system implementation, we define an executable semantics of the UPPAAL PORT components that guarantees that the implementation preserves the invariant properties of the model. Assuming a system implementation that conforms to the formal model, we investigate how to provide test cases suitable for the eventual verification of such implementation, by exploiting the model checker’s ability to generate witness traces for reachability verification. Such a witness trace represents a execution of the system from its initial state to the goal state encoded by the reachability property, and becomes our abstract test case. By pairing the automated model-based test case generator with an automatic transformation from the abstract test cases to Python scripts, we enable the execution of the generated Python scripts on the system under test, which ends up in pass/fail testing verdicts. Dependency analysis is a method that is able to identify crucial intra- and inter-component dependencies early in the system’s development life cycle, if applied on architectural models. In this thesis, we also investigate how such dependencies, resulting from applying dependency analysis on EAST-ADL models, can be exploited during formal verification in order to reduce the verified state-spaces during model checking. The framework is supported by the ViTAL tool and its applicability is shown on an automotive industrial prototype, namely a Brake-by-Wire system. 

Place, publisher, year, edition, pages
Västerås: Mälardalen University, 2016
Series
Mälardalen University Press Dissertations, ISSN 1651-4238 ; 206
National Category
Embedded Systems
Research subject
Computer Science
Identifiers
urn:nbn:se:mdh:diva-32463 (URN)978-91-7485-278-3 (ISBN)
External cooperation:
Public defence
2016-10-07, Gamma, Mälardalens högskola, Västerås, 13:15 (English)
Opponent
Supervisors
Available from: 2016-08-17 Created: 2016-08-17 Last updated: 2016-09-12Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopusLänktext

Search in DiVA

By author/editor
Enoiu, Eduard PaulMarinescu, RalucaSeceleanu, CristinaPettersson, Paul
By organisation
Embedded Systems
In the same journal
Reliability Engineering & System Safety
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 59 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf