nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Modelling and Analysing Software in mCRL2

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

Erschienen in: Formal Aspects of Component Software

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Modeling Guidelines for Component-Based Supervisory Control Synthesis

Nächstes Kapitel A Formally Verified Model of Web Components

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

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

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_7CrossRef

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

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_14CrossRef

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_2CrossRef

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_2CrossRef

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_29CrossRef

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

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_12CrossRef

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)CrossRef

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_13CrossRefMATH

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-systemsCrossRef

13.

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

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

15.

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

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.009CrossRef

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.357207CrossRefMATH

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_11CrossRef

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-9CrossRefMATH

23.

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

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.004CrossRef

25.

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

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)

27.

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

Titel: Modelling and Analysing Software in mCRL2
verfasst von: Jan Friso Groote
Jeroen J. A. Keiren
Bas Luttik
Erik P. de Vink
Tim A. C. Willemse
Verlag: Springer International Publishing
Buch: Formal Aspects of Component Software
Print ISBN: 978-3-030-40913-5

Electronic ISBN: 978-3-030-40914-2

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-40914-2_2

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"