Abstract
The advanced technology used for developing modern automotive systems increases their complexity, making their correctness assurance very tedious. To enable analysis by simulation, but also enhance understanding and communication, engineers use MATLAB/Simulink modeling during system development. In this paper, we provide further analysis means to industrial Simulink models by proposing a pattern-based, execution-order preserving transformation of Simulink blocks into the input language of UPPAAL Statistical Model checker, that is, timed (or hybrid) automata with stochastic semantics. The approach leads to being able to analyze complex Simulink models of automotive systems, and we report our experience with two vehicular systems, the Brake-by-Wire and the Adjustable Speed Limiter.
The original version of this chapter was revised: Figure 1a and 1b was corrected. The erratum to this chapter is available at DOI: 10.1007/978-3-319-48989-6_51
An erratum to this chapter can be found at http://dx.doi.org/10.1007/978-3-319-48989-6_51
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
References
Dabney, J.B., Harman, T.L.: Mastering Simulink. Pearson/Prentice Hall, Upper Saddle River (2004)
Legay, A., Traonouez, L.-M.: Statistical model checking of Simulink models with Plasma Lab. In: Artho, C., Ölveczky, P.C. (eds.) FTSCS 2015. CCIS, vol. 596, pp. 259–264. Springer, Heidelberg (2016). doi:10.1007/978-3-319-29510-7_15
David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B.: UPPAAL SMC tutorial. STTT J. 17(4), 397–415 (2015)
Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348–370. Springer, Heidelberg (2010). doi:10.1007/978-3-642-17511-4_20
Barnat, J., Beran, J., Brim, L., Kratochvíla, T., Ročkai, P.: Tool chain to support automated formal verification of avionics Simulink designs. In: Stoelinga, M., Pinger, R. (eds.) FMICS 2012. LNCS, vol. 7437, pp. 78–92. Springer, Heidelberg (2012). doi:10.1007/978-3-642-32469-7_6
Meenakshi, B., Bhatnagar, A., Roy, S.: Tool for translating Simulink models into input language of a model checker. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 606–620. Springer, Heidelberg (2006). doi:10.1007/11901433_33
Agrawal, A., Simon, G., Karsai, G.: Semantic translation of Simulink/Stateflow models to hybrid automata using graph transformations. ENTCS J. 109, 43–56 (2004)
Miller, S.P.: Bridging the gap between model-based development and model checking. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 443–453. Springer, Heidelberg (2009). doi:10.1007/978-3-642-00768-2_36
Manamcheri, K., Mitra, S., Bak, S., Caccamo, M.: A step towards verification and synthesis from Simulink/Stateflow models. In: HSCC 2011, pp. 317–318. ACM (2011)
Jiang, Y., Yang, Y., Liu, H., Kong, H., Gu, M., Sun, J., Sha, L.: From Stateflow simulation to verified implementation: a verification approach and a real-time train controller design. In: RTAS 2016, pp. 1–11, April 2016
David, A., Du, D., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B., Sedwards, S.: Statistical model checking for stochastic hybrid systems. arXiv preprint arXiv:1208.3856 (2012)
Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. STTT J. 1(1), 134–152 (1997)
Bulychev, P., David, A., Larsen, K.G., Legay, A., Li, G., Poulsen, D.B.: Rewrite-based statistical model checking of WMTL. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 260–275. Springer, Heidelberg (2013). doi:10.1007/978-3-642-35632-2_25
Acknowledgement
This work has been funded by the Swedish Governmental Agency for Innovation Systems (VINNOVA) under the VeriSpec project 2013-01299.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Filipovikj, P., Mahmud, N., Marinescu, R., Seceleanu, C., Ljungkrantz, O., Lönn, H. (2016). Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds) FM 2016: Formal Methods. FM 2016. Lecture Notes in Computer Science(), vol 9995. Springer, Cham. https://doi.org/10.1007/978-3-319-48989-6_46
Download citation
DOI: https://doi.org/10.1007/978-3-319-48989-6_46
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-48988-9
Online ISBN: 978-3-319-48989-6
eBook Packages: Computer ScienceComputer Science (R0)