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
Statistical Analysis of Resource Usage of Embedded Systems Modeled in EAST-ADL
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0002-7663-5497
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0003-2416-4205
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0003-2870-2680
2015 (English)In: IEEE Computer Society Annual Symposium on VLSI (ISVLSI), 2015, 380-385 p.Conference paper, Published paper (Refereed)
Abstract [en]

The growing complexity of modern automotive embedded systems requires new techniques for model-based design that takes under consideration both software and hardware constraints and enables verification at early stages of development. In this context, EAST-ADL was developed as a domain specific language dedicated to modeling of functional-, software-, and hardware- architecture of automotive embedded systems. This language represents a convenient abstraction when reasoning about the system functionality and supports modeling of relevant extra-functional properties, like timing and resource usage. By providing formal semantics to the EAST-ADL language, as a network of priced timed automata, it becomes possible to reason about feasibility and worst-case resource consumption of the embedded components. In this paper, we show how to analyze such embedded systems modeled in EAST-ADL by using statistical model-checking. We report our experiences from applying this approach to an industrial Brake-by-Wire system.

Place, publisher, year, edition, pages
2015. 380-385 p.
National Category
Computer Systems
Identifiers
URN: urn:nbn:se:mdh:diva-30439DOI: 10.1109/ISVLSI.2015.103ISI: 000377094100068Scopus ID: 2-s2.0-84956968739ISBN: 978-1-4799-8718-4 (print)OAI: oai:DiVA.org:mdh-30439DiVA: diva2:886130
Conference
IEEE Computer Society Annual Symposium on VLSI ISVLSI, 8-10 Jul 2015, Montpellier, France
Projects
ITS-EASY Post Graduate School for Embedded Software and SystemsVeriSpec - Structured Specification and Automated Verification for Automotive Functional SafetyTOCSYC - Testing of Critical System Characteristics (KKS)
Available from: 2015-12-21 Created: 2015-12-21 Last updated: 2016-08-17Bibliographically approved
In thesis
1. 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 textScopus

Search in DiVA

By author/editor
Marinescu, RalucaEnoiu, Eduard PaulSeceleanu, Cristina
By organisation
Embedded Systems
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 17 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