Advertisement

Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations

  • Johanna Nellen
  • Thomas Rambow
  • Md Tawhid Bin Waez
  • Erika Ábrahám
  • Joost-Pieter Katoen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10951)

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.

Notes

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.

References

  1. 1.
    MathWorks: Simulink Design Verifier. https://de.mathworks.com/products/sldesignverifier.html
  2. 2.
    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_15CrossRefGoogle Scholar
  3. 3.
    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_8CrossRefGoogle Scholar
  4. 4.
    Barnat, J., Bauch, P., Havel, V.: Temporal verification of Simulink diagrams. In: Proceedings of HASE 2014, pp. 81–88. IEEE (2014)Google Scholar
  5. 5.
    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_6CrossRefGoogle Scholar
  6. 6.
    Barnat, J., Brim, L., Beran, J.: Executing model checking counterexamples in Simulink. In: Proceedings of TASE 2012, pp. 245–248. IEEE (2012)Google Scholar
  7. 7.
    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_14CrossRefGoogle Scholar
  8. 8.
    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)Google Scholar
  9. 9.
    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_6CrossRefGoogle Scholar
  10. 10.
    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_7CrossRefGoogle Scholar
  11. 11.
    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)Google Scholar
  12. 12.
    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_3CrossRefGoogle Scholar
  13. 13.
    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_14CrossRefGoogle Scholar
  14. 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)Google Scholar
  15. 15.
    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)Google Scholar
  16. 16.
    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)Google Scholar
  17. 17.
    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)Google Scholar
  18. 18.
    MathWorks: Simulink Design Verifier - User’s guide. https://de.mathworks.com/help/pdf_doc/sldv/sldv_ug.pdf
  19. 19.
  20. 20.
    Prover Technology AB: Prover Plug-In. http://www.prover.com
  21. 21.
    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)Google Scholar
  22. 22.
    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)Google Scholar
  23. 23.
    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)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  • Johanna Nellen
    • 1
  • Thomas Rambow
    • 2
  • Md Tawhid Bin Waez
    • 3
  • Erika Ábrahám
    • 1
  • Joost-Pieter Katoen
    • 1
  1. 1.RWTH Aachen UniversityAachenGermany
  2. 2.Ford Werke GmbHCologneGermany
  3. 3.Ford Motor CompanyDearbornUSA

Personalised recommendations