Skip to main content
SpringerLink
Log in

Modelling and Analysing Software in mCRL2

  • Conference paper
  • First Online:
Formal Aspects of Component Software (FACS 2019)

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

Included in the following conference series:

Abstract

Model checking is an effective way to design correct software. Making behavioural models of software, formulating correctness properties using modal formulas, and verifying these using finite state analysis techniques, is a very efficient way to obtain the required insight in the software. We illustrate this on four common but tricky examples.

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.

    See for instance the online mCRL2 introductory tutorial on https://mcrl2.org/.

References

  1. https://github.com/mCRL2org/mCRL2/tree/master/examples/software_models

  2. Bartholomeus, M., Luttik, B., Willemse, T.: Modelling and analysing ERTMS hybrid level 3 with the mCRL2 toolset. In: Howar, F., Barnat, J. (eds.) FMICS 2018. LNCS, vol. 11119, pp. 98–114. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-00244-2_7

    Chapter  Google Scholar 

  3. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, Berlin (2004). https://doi.org/10.1007/978-3-662-07964-5

    Book  MATH  Google Scholar 

  4. 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 

  5. 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 

  6. 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 

  7. Cimatti, A., et al.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45657-0_29

    Chapter  Google Scholar 

  8. Dechev, D., Pirkelbauer, P., Stroustrup, B.: Understanding and effectively preventing the ABA problem in descriptor-based lock-free designs. In: 13th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing (ISORC 2010), Carmona, Sevilla, Spain, 5–6 May 2010, pp. 185–192. IEEE Computer Society (2010). https://doi.org/10.1109/ISORC.2010.10

  9. Ernst, G., Huisman, M., Mostowski, W., Ulbrich, M.: VerifyThis – verification competition with a human factor. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 176–195. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17502-3_12

    Chapter  Google Scholar 

  10. Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. STTT 15(2), 89–107 (2013)

    Article  Google Scholar 

  11. Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3—a modern refinement checker for CSP. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 187–201. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_13

    Chapter  MATH  Google Scholar 

  12. Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communicating Systems. MIT Press, Cambridge (2014). https://mitpress.mit.edu/books/modeling-and-analysis-communicating-systems

    Book  Google Scholar 

  13. Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137–161 (1985). https://doi.org/10.1145/2455.2460

    Article  MathSciNet  MATH  Google Scholar 

  14. Hitotumatu, H., Noshita, K.: A technique for implementing backtrack algorithms and its application. Inf. Process. Lett. 8(4), 174–175 (1979). https://doi.org/10.1016/0020-0190(79)90016-4

    Article  Google Scholar 

  15. Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997). https://doi.org/10.1109/32.588521

    Article  Google Scholar 

  16. Hwong, Y.L., Keiren, J.J.A., Kusters, V.J.J., Leemans, S., 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). https://doi.org/10.1016/j.scico.2012.11.009

    Article  Google Scholar 

  17. Keiren, J.J.A., Klabbers, M.D.: Modelling and verifying IEEE Std 11073–20601 session setup using mCRL2. Electron. Commun. EASST 53 (2013). https://doi.org/10.14279/tuj.eceasst.53.793

  18. Knuth, D.E.: Dancing links (2000). arXiv:cs/0011047

  19. Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. C-28(9), 690–691 (1979). https://doi.org/10.1109/TC.1979.1675439

  20. Lamport, L.: Specifying concurrent program modules. ACM Trans. Program. Lang. Syst. 5(2), 190–222 (1983). https://doi.org/10.1145/69624.357207

    Article  MATH  Google Scholar 

  21. Laveaux, M., Groote, J.F., Willemse, T.A.C.: Correct and efficient antichain algorithms for refinement checking. In: Pérez, J.A., Yoshida, N. (eds.) FORTE 2019. LNCS, vol. 11535, pp. 185–203. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-21759-4_11

    Chapter  Google Scholar 

  22. Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9

    Book  MATH  Google Scholar 

  23. Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115–116 (1981)

    Article  Google Scholar 

  24. Remenska, D., Willemse, T.A.C., Verstoep, K., Templon, J., Bal, H.: Using model checking to analyze the system behavior of the LHC production grid. Future Gener. Comput. Syst. 29(8), 2239–2251 (2013). https://doi.org/10.1016/j.future.2013.06.004

    Article  Google Scholar 

  25. Roscoe, A.W.: Understanding Concurrent Systems. Texts in Computer Science. Springer, London (2010). https://doi.org/10.1007/978-1-84882-258-0

    Book  MATH  Google Scholar 

  26. Treiber, R.K.: Systems programming: coping with parallelism. Technical Report RJ 5118 (53162). International Business Machines Incorporated, Thomas J. Watson Research Center, San Jose, California (1986)

    Google Scholar 

  27. Wikipedia. http://en.wikipedia.org/wiki/peterson’s_algorithm (2015). Accessed 17 May 2015

Download references

Author information

Authors and Affiliations

  1. Faculty of Mathematics and Computer Science, Eindhoven University of Technology, Eindhoven, The Netherlands

    Jan Friso Groote, Jeroen J. A. Keiren, Bas Luttik, Erik P. de Vink & Tim A. C. Willemse

Authors
  1. Jan Friso Groote
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jeroen J. A. Keiren
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Bas Luttik
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Erik P. de Vink
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Tim A. C. Willemse
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Tim A. C. Willemse .

Editor information

Editors and Affiliations

  1. CWI, University of Leiden, Leiden, The Netherlands

    Farhad Arbab

  2. Open University of the Netherlands, Heerlen, The Netherlands

    Sung-Shik Jongmans

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

Groote, J.F., Keiren, J.J.A., Luttik, B., de Vink, E.P., Willemse, T.A.C. (2020). Modelling and Analysing Software in mCRL2. In: Arbab, F., Jongmans, SS. (eds) Formal Aspects of Component Software. FACS 2019. Lecture Notes in Computer Science(), vol 12018. Springer, Cham. https://doi.org/10.1007/978-3-030-40914-2_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-40914-2_2

  • Published:

  • Publisher Name: Springer, Cham

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation