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
Analyzing Industrial Architectural Models by Simulation and Model-Checking
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0002-7663-5497
Volvo Group Trucks Technology, Gothenburg, Sweden .
Aalborg University, Denmark.
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0003-2870-2680
Show others and affiliations
2015 (English)In: Communications in Computer and Information Science, vol. 476, 2015, 2015, 189-205 p.Conference paper, Published paper (Refereed)
Abstract [en]

The software architecture of any automotive system has to be decided well in advance of production, so it is very desirable to assess its quality in order to obtain quick indications of errors at early design phases. In this paper, we present a constellation of analysis techniques for architectural models described in EAST-ADL. The methods are complementary in terms of covering EAST-ADL model analysis against a rich set of requirements, and in terms of the varying degree of confidence in the provided guarantees. Based on the needs of the current model- driven development in a chosen automotive context, we propose three analysis techniques of EAST-ADL architectural models, in an attempt to tackle some of the exposed design needs: simulation of EAST-ADL functions in Simulink, model-checking EAST-ADL models with timed automata semantics, and statistical model-checking in UPPAAL, applied on an automatically generated network of timed automata. An indus- trial Brake-by-Wire prototype is the case study on which we show the potential of simulating EAST-ADL models in Simulink, model-checking downscale EAST-ADL models, as well statistical model-checking of full model versions, in order to tame verification scalability problems.

Place, publisher, year, edition, pages
2015. 189-205 p.
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
URN: urn:nbn:se:mdh:diva-26801DOI: 10.1007/978-3-319-17581-2_13ISI: 000368430500013Scopus ID: 2-s2.0-84929618771ISBN: 978-331917580-5 (print)OAI: oai:DiVA.org:mdh-26801DiVA: diva2:768217
Conference
Third International Workshop on Formal Techniques for Safety-Critical Systems FTSCS2014, 6-7 Nov 2014, Luxembourg, Luxemburg
Projects
MBAT - Combined Model-based Analysis and Testing (Artemis/Vinnova)
Available from: 2014-12-03 Created: 2014-12-02 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, RalucaSeceleanu, Cristina
By organisation
Embedded Systems
Electrical Engineering, Electronic Engineering, Information Engineering

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

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