Abstract
The automotive industry makes increasing usage of Simulink-based software development. Typically, automotive Simulink designs are analyzed using non-formal test methods, which do not guarantee the absence of errors. In contrast, formal verification techniques aim at providing formal guarantees or counterexamples that the analyzed designs fulfill their requirements for all possible inputs and parameters. Therefore, the automotive safety standard ISO 26262 recommends the usage of formal methods in safety-critical software development.
In this paper, we report on the application of formal verification to check discrete-time properties of a Simulink model for a park assistant R&D prototype feature using the commercial Simulink Design Verifier tool. During our evaluation, we experienced a gap between the offered functionalities and typical industrial needs, which hindered the successful application of this tool in the context of model-based development. We discuss these issues and propose solutions related to system development, requirements specification and verification tools, in order to prepare the ground for the effective integration of computer-assisted formal verification in automotive Simulink-based development.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
MathWorks: Simulink Design Verifier. https://de.mathworks.com/products/sldesignverifier.html
Gholami, M.-R., Boucheneb, H.: Applying formal methods into safety-critical health applications. In: Ortmeier, F., Rauzy, A. (eds.) IMBSA 2014. LNCS, vol. 8822, pp. 195–208. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-12214-4_15
Boström, P., Heikkilä, M., Huova, M., Waldén, M., Linjama, M.: Verification and validation of a pressure control unit for hydraulic systems. In: Majzik, I., Vieira, M. (eds.) SERENE 2014. LNCS, vol. 8785, pp. 101–115. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-12241-0_8
Barnat, J., Bauch, P., Havel, V.: Temporal verification of Simulink diagrams. In: Proceedings of HASE 2014, pp. 81–88. IEEE (2014)
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). https://doi.org/10.1007/978-3-642-32469-7_6
Barnat, J., Brim, L., Beran, J.: Executing model checking counterexamples in Simulink. In: Proceedings of TASE 2012, pp. 245–248. IEEE (2012)
Reicherdt, R., Glesner, S.: Formal verification of discrete-time MATLAB/simulink models using boogie. In: Giannakopoulou, D., Salaün, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 190–204. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10431-7_14
Herber, P., Reicherdt, R., Bittner, P.: Bit-precise formal verification of discrete-time MATLAB/Simulink models using SMT solving. In: Proceedings of EMSOFT 2013, pp. 1–10. IEEE (2013)
Cofer, D.: Model checking: cleared for take off. In: van de Pol, J., Weber, M. (eds.) SPIN 2010. LNCS, vol. 6349, pp. 76–87. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16164-3_6
Whalen, M., Cofer, D., Miller, S., Krogh, B.H., Storm, W.: Integration of formal analysis into a model-based software development process. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol. 4916, pp. 68–84. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-79707-4_7
Bourbouh, H., Garoche, P.L., Garion, C., Gurfinkel, A., Kahsai, T., Thirioux, X.: Automated analysis of Stateflow models. In: Proceedings of LPAR 2017. EPiC Series in Computing, vol. 46, pp. 144–161. EasyChair (2017)
Dragomir, I., Preoteasa, V., Tripakis, S.: Compositional semantics and analysis of hierarchical block diagrams. In: Bošnački, D., Wijs, A. (eds.) SPIN 2016. LNCS, vol. 9641, pp. 38–56. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-32582-8_3
Preoteasa, V., Dragomir, I., Tripakis, S.: Type inference of simulink hierarchical block diagrams in Isabelle. In: Bouajjani, A., Silva, A. (eds.) FORTE 2017. LNCS, vol. 10321, pp. 194–209. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-60225-7_14
Ali, S., Sulyman, M.: Applying model checking for verifying the functional requirements of a Scania’s vehicle control system. Master’s thesis, Mälardalen University (2012)
Botham, J., Dhadyalla, G., Powell, A., Miller, P., Haas, O., McGeoch, D., Rao, A.C., O’Halloran, C., Kiec, J., Farooq, A., Poushpas, S., Tudor, N.: PICASSOS - Practical applications of automated formal methods to safety related automotive systems. In: SAE Technical Paper, SAE International (2017)
Bennion, M., Habli, I.: A candid industrial evaluation of formal software verification using model checking. In: Proceedings of ICSE Companion 2014, pp. 175–184. ACM (2014)
Berger, P., Katoen, J.P., Ábrahám, E., Waez, M.T.B., Rambow, T.: Verifiying auto-generated C code from Simulink – an experience report in the automotive domain. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 312–328. Springer, Cham (2018)
MathWorks: Simulink Design Verifier - User’s guide. https://de.mathworks.com/help/pdf_doc/sldv/sldv_ug.pdf
MathWorks: Polyspace. http://www.mathworks.com/products/polyspace/
Prover Technology AB: Prover Plug-In. http://www.prover.com
Bozzano, M., Bruintjes, H., Cimatti, A., Katoen, J.P., Noll, T., Tonetta, S.: The compass 3.0 toolset (short paper). In: Proceedings of IMBSA 2017 (2017)
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of ICSE 1999, pp. 411–420. ACM (1999)
Autili, M., Grunske, L., Lumpe, M., Pelliccione, P., Tang, A.: Aligning qualitative, real-time, and probabilistic property specification patterns using a structured english grammar. IEEE Trans. Softw. Eng. 41(7), 620–638 (2015)
Acknowledgments
The authors want to thank Petter Nilsson, Philipp Berger, William Milam and Cem Mengi for numerous fruitful discussions on Simulink verification. We also express our appreciation to the MathWorks support team for their fast response and helpful advice.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Nellen, J., Rambow, T., Waez, M.T.B., Ábrahám, E., Katoen, JP. (2018). Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds) Formal Methods. FM 2018. Lecture Notes in Computer Science(), vol 10951. Springer, Cham. https://doi.org/10.1007/978-3-319-95582-7_23
Download citation
DOI: https://doi.org/10.1007/978-3-319-95582-7_23
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-95581-0
Online ISBN: 978-3-319-95582-7
eBook Packages: Computer ScienceComputer Science (R0)