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 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
The Functional Mock-up Interface (FMI) is a tool-independent standard to support behavior models using a combination of xml-files and compiled C-code. The standard defines the concept of a Functional Mock-up Unit (FMU), as a software component that implements the FMI standard.
References
Eclipse. The EAST-ADL Tool Platform (EATOP) Editor Tool (2014). http://www.eclipse.org/proposals/modeling.eatop/
Mathworks. The MATLAB Simulink Design Tool (2014). http://www.mathworks.se/products/simulink/
Modelica Association Project. The Functional Mock-up Interface (FMI) Standard (2014). http://www.fmi-standard.org/
The AUTomotive Open System ARchitecture (AUTOSAR) (2014). http://www.autosar.org/
Alur, R.: Timed automata. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 8–22. Springer, Heidelberg (1999)
Biehl, M., Sjöstedt, C.-J., Törngren, M.: A modular tool integration approach- experiences from two case studies. In: 3rd Workshop on Model-Driven Tool & Process Integration at the European Conference on Modelling Foundations and Applications (2010)
Blom, H., Lönn, H., Hagl, F., Papadopoulos, Y., Reiser, M.-O., Sjöstedt, C.-J., Chen, D.J., Tagliabò, F., Torchiaro, S., Tucci, S.: EAST-ADL: An architecture description language for automotive software-intensive systems. EAST-ADL WhitePaper, vol. 1 (2013)
Cuenot, P., Chen, D., Gerard, S., Lonn, H., Reiser, M.-O., Servat, D., Sjostedt, C.-J., Kolagari, R.T., Torngren, M., Weber, M.: Managing complexity of automotive electronics using the EAST-ADL. In: 12th IEEE International Conference on Engineering Complex Computer Systems, pp. 353–358. IEEE (2007)
David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B., van Vliet, J., Wang, Z.: Statistical model checking for networks of priced timed automata. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 80–96. Springer, Heidelberg (2011)
David, A., Larsen, K.G., Legay, A., Mikučionis, M., Wang, Z.: Time for statistical model checking of real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 349–355. Springer, Heidelberg (2011)
David, A., Larsen, K.G., Legay, A., Mikučionis, M.: Schedulability of herschel-planck revisited using statistical model checking. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part II. LNCS, vol. 7610, pp. 293–307. Springer, Heidelberg (2012)
Feng, L., Chen, D., Lönn, H., Torngren, M.: Verifying system behaviors in EAST-ADL2 with the SPIN model checker. In: International Conference on Mechatronics and Automation, pp. 144–149 (2010)
Kang, E.-Y., Enoiu, E.P., Marinescu, R., Seceleanu, C., Schobbens, P.-Y., Pettersson, P.: A methodology for formal analysis and verification of EAST-ADL models. Reliab. Eng. Syst. Saf. Int. J. 120, 127–138 (2013)
Mallet, F., Peraldi-Frati, M.-A., André, C.: Marte CCSL to execute EAST-ADL timing requirements. In: International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing, pp. 249–253. IEEE (2009)
Qureshi, T.N., Chen, D.-J., Persson, M., Trngren, M.: On integrating EAST-ADL and UPPAAL for embedded system architecture verification. In: Sangiovanni-Vincentelli, A. (ed.) Embedded Systems Development, vol. 20. Springer, New York (2014)
Acknowledgment
The research leading to these results has received funding from the ARTEMIS Joint Undertaking under grant agreement number 269335, and from VINNOVA, the Swedish Governmental Agency for Innovation Systems, within the MBAT project.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Marinescu, R., Kaijser, H., Mikučionis, M., Seceleanu, C., Lönn, H., David, A. (2015). Analyzing Industrial Architectural Models by Simulation and Model-Checking. In: Artho, C., Ölveczky, P. (eds) Formal Techniques for Safety-Critical Systems. FTSCS 2014. Communications in Computer and Information Science, vol 476. Springer, Cham. https://doi.org/10.1007/978-3-319-17581-2_13
Download citation
DOI: https://doi.org/10.1007/978-3-319-17581-2_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-17580-5
Online ISBN: 978-3-319-17581-2
eBook Packages: Computer ScienceComputer Science (R0)