TY - GEN
T1 - Analyzing industrial architectural models by simulation and model-checking
AU - Marinescu, Raluca
AU - Kaijser, Henrik
AU - Mikučionis, Marius
AU - Seceleanu, Cristina
AU - Lönn, Henrik
AU - David, Alexandre
PY - 2015
Y1 - 2015
N2 - 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
AB - 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
U2 - 10.1007/978-3-319-17581-2_13
DO - 10.1007/978-3-319-17581-2_13
M3 - Article in proceeding
AN - SCOPUS:84929618771
SN - 978-3-319-17580-5
T3 - Communications in Computer and Information Science
SP - 189
EP - 205
BT - Formal Techniques for Safety-Critical Systems
A2 - Artho, Cyrille
A2 - Ölevczky, Peter Csaba
PB - Springer
T2 - 3rd International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2014
Y2 - 6 November 2014 through 7 November 2014
ER -