Analyzing industrial architectural models by simulation and model-checking

Raluca Marinescu*, Henrik Kaijser, Marius Mikučionis, Cristina Seceleanu, Henrik Lönn, Alexandre David

*Corresponding author for this work

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

17 Citations (Scopus)


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 modeldriven 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 industrial 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

Original languageEnglish
Title of host publicationFormal Techniques for Safety-Critical Systems : Third International Workshop, FTSCS 2014, Luxembourg, November 6-7, 2014. Revised Selected Papers
EditorsCyrille Artho, Peter Csaba Ölevczky
Number of pages17
Publication date2015
ISBN (Print)978-3-319-17580-5
ISBN (Electronic)978-3-319-17581-2
Publication statusPublished - 2015
Event3rd International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2014 - Luxembourg, Luxembourg
Duration: 6 Nov 20147 Nov 2014


Conference3rd International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2014
SeriesCommunications in Computer and Information Science


Dive into the research topics of 'Analyzing industrial architectural models by simulation and model-checking'. Together they form a unique fingerprint.

Cite this