Skip to main content
SpringerLink
Log in

Formal Verification of OIL Component Specifications using mCRL2

  • Conference paper
  • First Online:
Formal Methods for Industrial Critical Systems (FMICS 2020)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 12327))

Abstract

To aid in making software bug-free, several high-tech companies are moving from coding to modelling. In some cases model checking techniques are explored or have already been adopted to get more value from these models. This also holds for Canon Production Printing, where the language OIL was developed for modelling control-software components. In this paper we present OIL and give its semantics. We define a translation from OIL to mCRL2 to enable the use of model checking techniques. Moreover, we discuss informal validity requirements on OIL component specifications and show how these can be formalised and verified using model checking. To test the feasibility of these techniques, we apply them to two models of systems used in production.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    https://github.com/MetaBorgCube/metaborg-mcrl2.

  2. 2.

    As mentioned earlier, the mCRL2 toolset tends to run slower on Windows machines. This is mostly because the compiling rewriter (passing option -rjittyc to lps2lts, the state space generation tool), which is typically much faster than the default rewriter, is not available on Windows machines. To experiment what improvement the compiling rewriter could bring we used a virtual machine running Ubuntu 20.04 and using half the laptop’s memory. On this virtual machine the LTS can be generated in 6 min from the mCRL2 specification using the options -bo for mcrl22lps and the option -rjittyc for lps2lts.

References

  1. Axelsson, R., Lange, M., Somla, R.: The complexity of model checking higher-order fixpoint logic. Logical Methods Comput. Sci. 3(2), 7 (2007)

    MathSciNet  Google Scholar 

  2. Basile, D., ter Beek, M.H., Ferrari, A., Legay, A.: Modelling and analysing ERTMS L3 moving block railway signalling with simulink and Uppaal SMC. In: Larsen, K.G., Willemse, T. (eds.) FMICS 2019. LNCS, vol. 11687, pp. 1–21. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-27008-7_1

    Chapter  Google Scholar 

  3. ter Beek, M.H., et al.: Adopting formal methods in an industrial setting: the railways case. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 762–772. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30942-8_46

    Chapter  Google Scholar 

  4. ter Beek, M.H., de Vink, E.P., Willemse, T.A.C.: Family-based model checking with mCRL2. In: Huisman, M., Rubin, J. (eds.) FASE 2017. LNCS, vol. 10202, pp. 387–405. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54494-5_23

    Chapter  Google Scholar 

  5. Berger, U., James, P., Lawrence, A., Roggenbach, M., Seisenberger, M.: Verification of the European rail traffic management system in real-time Maude. Sci. Comput. Program. 154, 61–88 (2018)

    Article  Google Scholar 

  6. van Beusekom, R., et al.: Formalising the Dezyne modelling language in mCRL2. In: Petrucci, L., Seceleanu, C., Cavalcanti, A. (eds.) FMICS/AVoCS -2017. LNCS, vol. 10471, pp. 217–233. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67113-0_14

    Chapter  Google Scholar 

  7. Bouwman, M., Janssen, B., Luttik, B.: Formal modelling and verification of an interlocking using mCRL2. In: Larsen, K.G., Willemse, T. (eds.) FMICS 2019. LNCS, vol. 11687, pp. 22–39. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-27008-7_2

    Chapter  Google Scholar 

  8. Bravenboer, M., Kalleberg, K.T., Vermaas, R., Visser, E.: Stratego/XT 0.17. A language and toolset for program transformation. Sci. Comput. Program. 72(1–2), 52–70 (2008)

    Google Scholar 

  9. Bunte, O., van Gool, L.C.M., Willemse, T.A.C.: Semantics and model checking of OIL component specifications. Technical report, Eindhoven University of Technology (2020)

    Google Scholar 

  10. Bunte, O., et al.: The mCRL2 toolset for analysing concurrent systems. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 21–39. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17465-1_2

    Chapter  Google Scholar 

  11. Cordy, M., et al.: A decade of featured transition systems. In: ter Beek, M.H., Fantechi, A., Semini, L. (eds.) From Software Engineering to Formal Methods and Tools, and Back. LNCS, vol. 11865, pp. 285–312. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30985-5_18

    Chapter  Google Scholar 

  12. Csertán, G., Huszerl, G., Majzik, I., Pap, Z., Pataricza, A., Varró, D.: VIATRA - visual automated transformations for formal verification and validation of UML models. In: ASE, pp. 267–270. IEEE Computer Society (2002)

    Google Scholar 

  13. Denkers, J., van Gool, L., Visser, E.: Migrating custom DSL implementations to a language workbench (tool demo). In: SLE, pp. 205–209. ACM (2018)

    Google Scholar 

  14. Fernandez, J., Bozga, M., Ghirvu, L.: State space reduction based on live variables analysis. Sci. Comput. Program. 47(2–3), 203–220 (2003)

    Article  MathSciNet  Google Scholar 

  15. Frenken, M.: Code generation and model-based testing in context of OIL. Master’s thesis, Eindhoven University of Technology (2019)

    Google Scholar 

  16. van Gool, L.: Formalising interface specifications. Ph.D. thesis, Eindhoven University of Technology (2006)

    Google Scholar 

  17. Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communicating Systems. MIT Press, Cambridge (2014)

    Book  Google Scholar 

  18. Groote, J.F., Willemse, T.A.C.: Parameterised boolean equation systems. Theor. Comput. Sci. 343(3), 332–369 (2005)

    Article  MathSciNet  Google Scholar 

  19. Hansen, H.H., Ketema, J., Luttik, B., Mousavi, M.R., van de Pol, J.: Towards model checking executable UML specifications in mCRL2. Innovations Syst. Softw. Eng. 6(1–2), 83–90 (2010). https://doi.org/10.1007/s11334-009-0116-1

    Article  Google Scholar 

  20. Hwong, Y., Keiren, J.J.A., Kusters, V.J.J., Leemans, S.J.J., Willemse, T.A.C.: Formalising and analysing the control software of the compact muon solenoid experiment at the Large Hadron Collider. Sci. Comput. Program. 78(12), 2435–2452 (2013)

    Article  Google Scholar 

  21. Islam, M.A., Cleaveland, R., Fenton, F.H., Grosu, R., Jones, P.L., Smolka, S.A.: Probabilistic reachability for multi-parameter bifurcation analysis of cardiac alternans. Theor. Comput. Sci. 765, 158–169 (2019)

    Article  MathSciNet  Google Scholar 

  22. Kernberger, D., Lange, M.: Model checking for hybrid branching-time logics. J. Logic. Algebraic Methods Program. 110, 100427 (2020)

    Article  MathSciNet  Google Scholar 

  23. Kim, J.H., Larsen, K.G., Nielsen, B., Mikučionis, M., Olsen, P.: Formal analysis and testing of real-time automotive systems using UPPAAL tools. In: Núñez, M., Güdemann, M. (eds.) FMICS 2015. LNCS, vol. 9128, pp. 47–61. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-19458-5_4

    Chapter  Google Scholar 

  24. Kölbl, M., Leue, S.: Automated functional safety analysis of automated driving systems. In: Howar, F., Barnat, J. (eds.) FMICS 2018. LNCS, vol. 11119, pp. 35–51. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-00244-2_3

    Chapter  Google Scholar 

  25. Latella, D., Majzik, I., Massink, M.: Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker. Formal Aspects Comput. 11(6), 637–664 (1999). https://doi.org/10.1007/s001659970003

    Article  Google Scholar 

  26. Limbrée, C., Cappart, Q., Pecheur, C., Tonetta, S.: Verification of railway interlocking - compositional approach with OCRA. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds.) RSSRail 2016. LNCS, vol. 9707, pp. 134–149. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33951-1_10

    Chapter  Google Scholar 

  27. Mitsch, S., Gario, M., Budnik, C.J., Golm, M., Platzer, A.: Formal verification of train control with air pressure brakes. In: Fantechi, A., Lecomte, T., Romanovsky, A. (eds.) Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. RSSRail 2017. Lecture Notes in Computer Science, vol. 10598, pp. 173–191. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68499-4_12

  28. van de Pol, J., Timmer, M.: State space reduction of linear processes using control flow reconstruction. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 54–68. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04761-9_5

    Chapter  Google Scholar 

  29. Remenska, D., et al.: From UML to process algebra and back: an automated approach to model-checking software design artifacts of concurrent systems. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 244–260. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38088-4_17

    Chapter  Google Scholar 

  30. Sankaranarayanan, S., Kumar, S.A., Cameron, F., Bequette, B.W., Fainekos, G.E., Maahs, D.M.: Model-based falsification of an artificial pancreas control system. SIGBED Rev. 14(2), 24–33 (2017)

    Article  Google Scholar 

  31. Schäfer, T., Knapp, A., Merz, S.: Model checking UML state machines and collaborations. Electron. Notes Theor. Comput. Sci. 55(3), 357–369 (2001)

    Article  Google Scholar 

  32. Schrammel, P., Kroening, D., Brain, M., Martins, R., Teige, T., Bienmüller, T.: Successful use of incremental BMC in the automotive industry. In: Núñez, M., Güdemann, M. (eds.) FMICS 2015. LNCS, vol. 9128, pp. 62–77. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-19458-5_5

    Chapter  Google Scholar 

  33. Silva, J.: A vocabulary of program slicing-based techniques. ACM Comput. Surv. 44(3), 12:1–12:41 (2012)

    Article  Google Scholar 

  34. Toennemann, J., Rausch, A., Howar, F., Cool, B.: Checking consistency of real-time requirements on distributed automotive control software early in the development process using UPPAAL. In: Howar, F., Barnat, J. (eds.) FMICS 2018. LNCS, vol. 11119, pp. 67–82. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-00244-2_5

    Chapter  Google Scholar 

  35. Valmari, A.: Bisimilarity minimization in O(m logn) time. In: Franceschinis, G., Wolf, K. (eds.) PETRI NETS 2009. LNCS, vol. 5606, pp. 123–142. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02424-5_9

    Chapter  Google Scholar 

  36. Visser, E., et al.: A language designer’s workbench: a one-stop-shop for implementation and verification of language designs. In: Onward!, pp. 95–111. ACM (2014)

    Google Scholar 

  37. Zhang, S.J., Liu, Y.: An automatic approach to model checking UML state machines. In: SSIRI (Companion), pp. 1–6. IEEE Computer Society (2010)

    Google Scholar 

Download references

Acknowledgements

We thank Canon Production Printing for funding the VOICE-B project, of which this work is part of. We thank Jasper Denkers for his help with understanding Spoofax and its languages and for his remarks on this paper. We thank the reviewers for their helpful comments.

Author information

Authors and Affiliations

  1. Eindhoven University of Technology, Eindhoven, The Netherlands

    Olav Bunte & Tim A. C. Willemse

  2. Canon Production Printing, Venlo, The Netherlands

    Louis C. M. van Gool

Authors
  1. Olav Bunte
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Louis C. M. van Gool
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Tim A. C. Willemse
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Olav Bunte .

Editor information

Editors and Affiliations

  1. ISTI, Consiglio Nazionale delle Ricerche, Pisa, Italy

    Maurice H. ter Beek

  2. AIT Austrian Institute of Technology GmbH, Vienna, Austria

    Dejan Ničković

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Bunte, O., Gool, L.C.M.v., Willemse, T.A.C. (2020). Formal Verification of OIL Component Specifications using mCRL2. In: ter Beek, M.H., Ničković, D. (eds) Formal Methods for Industrial Critical Systems. FMICS 2020. Lecture Notes in Computer Science(), vol 12327. Springer, Cham. https://doi.org/10.1007/978-3-030-58298-2_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-58298-2_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-58297-5

  • Online ISBN: 978-3-030-58298-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation