You are required to read and agree to the below before accessing a full-text version of an article in the IDE article repository.

The full-text document you are about to access is subject to national and international copyright laws. In most cases (but not necessarily all) the consequence is that personal use is allowed given that the copyright owner is duly acknowledged and respected. All other use (typically) require an explicit permission (often in writing) by the copyright owner.

For the reports in this repository we specifically note that

  • the use of articles under IEEE copyright is governed by the IEEE copyright policy (available at http://www.ieee.org/web/publications/rights/copyrightpolicy.html)
  • the use of articles under ACM copyright is governed by the ACM copyright policy (available at http://www.acm.org/pubs/copyright_policy/)
  • technical reports and other articles issued by M‰lardalen University is free for personal use. For other use, the explicit consent of the authors is required
  • in other cases, please contact the copyright owner for detailed information

By accepting I agree to acknowledge and respect the rights of the copyright owner of the document I am about to access.

If you are in doubt, feel free to contact webmaster@ide.mdh.se

Analyzing Industrial Architectural Models by Simulation and Model-Checking

Fulltext:


Authors:

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

Research groups:

Software Testing Laboratory
Formal Modelling and Analysis of Embedded Systems

Publication Type:

Conference/Workshop Paper

Venue:

Third International Workshop on Formal Techniques for Safety-Critical Systems

Abstract

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.

Bibtex

@inproceedings{Marinescu3762,
author = {Raluca Marinescu and Henrik Kaijser and Marius Miku{\`e}ionis and Cristina Seceleanu and Henrik L{\"o}nn and Alexandre David},
title = {Analyzing Industrial Architectural Models by Simulation and Model-Checking},
month = {November},
year = {2014},
booktitle = {Third International Workshop on Formal Techniques for Safety-Critical Systems},
url = {http://www.es.mdu.se/publications/3762-}
}