nach oben

Erschienen in:

2021 | OriginalPaper | Buchkapitel

Tutorial: Designing Distributed Software in mCRL2

verfasst von : Jan Friso Groote, Jeroen J. A. Keiren

Erschienen in: Formal Techniques for Distributed Objects, Components, and Systems

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

Distributed software is very tricky to implement correctly as some errors only occur in peculiar situations. For such errors testing is not effective. Mathematically proving correctness is hard and time consuming, and therefore, it is rarely done. Fortunately, there is a technique in between, namely model checking, that, if applied with skill, is both efficient and able to find rare errors.

In this tutorial we show how to create behavioural models of parallel software, how to specify requirements using modal formulas, and how to verify these. For that we use the mCRL2 language and toolset (www.mcrl2.org/). We discuss the design of an evolution of well-known mutual exclusion protocols, and how model checking not only provides insight in their behaviour and correctness, but also guides their design.

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 Better Late Than Never or: Verifying Asynchronous Components at Runtime

In this paper, for the sake of brevity, we generally refer to parallel or distributed software just using the term distributed software. The techniques discussed in this paper apply equally in both situations.

In [12], variables \( LA \) and \( LB \) are used as flags, and a Boolean variable \( AP \) is used in the place of \( turn \).

Note that, alternatively, the multi-actions in mCRL2 could be used to combine fetching the value and evaluating the condition, see, e.g., [5].

Apt, K.R., Olderog, E.: Fifty years of Hoare’s logic. Formal Aspects Comput. 31(6), 751–807 (2019). https://doi.org/10.1007/s00165-019-00501-3

Bergstra, J.A., Klop, J.W.: The algebra of recursively defined processes and the algebra of regular processes. In: Paredaens, J. (ed.) ICALP 1984. LNCS, vol. 172, pp. 82–94. Springer, Heidelberg (1984). https://doi.org/10.1007/3-540-13345-3_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, Heidelberg (2004). https://doi.org/10.1007/978-3-662-07964-5

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., Luttik, B., Schols, W., Willemse, T.A.C.: A process algebra with global variables. In: Dardha, O., Rot, J. (eds.) Proceedings Combined 27th International Workshop on Expressiveness in Concurrency and 17th Workshop on Structural Operational Semantics, EXPRESS/SOS 2020, and 17th Workshop on Structural Operational Semantics. EPTCS, vol. 322, pp. 33–50 (2020). https://doi.org/10.4204/EPTCS.322.5

Bouwman, M., Luttik, B., Willemse, T.A.C.: Off-the-shelf automated analysis of liveness properties for just paths. Acta Informatica 57(3–5), 551–590 (2020). https://doi.org/10.1007/s00236-020-00371-w

Bradfield, J.C., Stirling, C.: Modal mu-calculi. In: Blackburn, P., van Benthem, J.F.A.K., Wolter, F. (eds.) Handbook of Modal Logic, Studies in Logic and Practical Reasoning, vol. 3, pp. 721–756. North-Holland (2007). https://doi.org/10.1016/s1570-2464(07)80015-2

van den Brand, M., Groote, J.F.: Software engineering: redundancy is key. Sci. Comput. Program. 97, 75–81 (2015). https://doi.org/10.1016/j.scico.2013.11.020

Cicirelli, F., Nigro, L., Sciammarella, P.F.: Model checking mutual exclusion algorithms using Uppaal. In: Silhavy, R., Senkerik, R., Oplatkova, Z.K., Silhavy, P., Prokopova, Z. (eds.) Software Engineering Perspectives and Application in Intelligent Systems. AISC, vol. 465, pp. 203–215. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33622-0_19CrossRef

10.

Cranen, S., Groote, J.F., Reniers, M.A.: A linear translation from CTL* to the first-order modal \(\mu \)-calculus. Theor. Comput. Sci. 412(28), 3129–3139 (2011). https://doi.org/10.1016/j.tcs.2011.02.034

11.

Dijkstra, E.W.: Solution of a problem in concurrent programming control. Commun. ACM 8(9), 569 (1965). https://doi.org/10.1145/365559.365617CrossRef

12.

Dijkstra, E.W.: Over de sequentialiteit van procesbeschrijvingen (Undated, 1962 or 1963)

13.

Dyseryn, V., van Glabbeek, R.J., Höfner, P.: Analysing mutual exclusion using process algebra with signals. In: Peters, K., Tini, S. (eds.) Proceedings Combined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics, EXPRESS/SOS 2017, Berlin, Germany, 4th September 2017. EPTCS, vol. 255, pp. 18–34 (2017). https://doi.org/10.4204/EPTCS.255.2

14.

Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. Int. J. Softw. Tools Technol. Transf. 15(2), 89–107 (2013). https://doi.org/10.1007/s10009-012-0244-z

15.

Gibson-Robinson, T., Armstrong, P.J., Boulgakov, A., Roscoe, A.W.: FDR3: a parallel refinement checker for CSP. Int. J. Softw. Tools Technol. Transf. 18(2), 149–167 (2016). https://doi.org/10.1007/s10009-015-0377-y

16.

Groote, J.F., Keiren, J.J.A., Luttik, B., de Vink, E.P., Willemse, T.A.C.: Modelling and analysing software in mCRL2. In: Arbab, F., Jongmans, S.-S. (eds.) FACS 2019. LNCS, vol. 12018, pp. 25–48. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-40914-2_2CrossRef

17.

Groote, J.F., Kouters, T.W.D.M., Osaiweran, A.: Specification guidelines to avoid the state space explosion problem. Softw. Test. Verification Reliab. 25(1), 4–33 (2015). https://doi.org/10.1002/stvr.1536

18.

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

19.

Groote, J.F., de Vink, E.P.: Problem solving using process algebra considered insightful. In: Katoen, J.-P., Langerak, R., Rensink, A. (eds.) ModelEd, TestEd, TrustEd. LNCS, vol. 10500, pp. 48–63. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68270-9_3CrossRef

20.

Groote, J.F., Wiedijk, F., Zantema, H.: A probabilistic analysis of the game of the goose. SIAM Rev. 58(1), 143–155 (2016). https://doi.org/10.1137/140983781

21.

Groote, J.F., Willemse, T.A.C.: A symmetric protocol to establish service level agreements. Log. Methods Comput. Sci. 16(3) (2020). https://lmcs.episciences.org/6812

22.

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

23.

Hopcroft, P.J., Broadfoot, G.H.: Combining the box structure development method and CSP for software development. Electron. Notes Theor. Comput. Sci. 128(6), 127–144 (2005). https://doi.org/10.1016/j.entcs.2005.04.008

24.

Leino, K.R.M., Wüstholz, V.: The Dafny integrated development environment. In: Dubois, C., Giannakopoulou, D., Méry, D. (eds.) Proceedings 1st Workshop on Formal Integrated Development Environment, F-IDE 2014, Grenoble, France, 6 April 2014. EPTCS, vol. 149, pp. 3–15 (2014). https://doi.org/10.4204/EPTCS.149.2

25.

Mateescu, R., Serwe, W.: Model checking and performance evaluation with CADP illustrated on shared-memory mutual exclusion protocols. Sci. Comput. Program. 78(7), 843–861 (2013). https://doi.org/10.1016/j.scico.2012.01.003

26.

Milner, R.: Communication and concurrency. PHI Series in Computer Science. Prentice Hall, Upper Saddle River (1989)

27.

Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9CrossRefMATH

28.

Osaiweran, A., Schuts, M., Hooman, J.: Experiences with incorporating formal techniques into industrial practice. Empir. Softw. Eng. 19(4), 1169–1194 (2014). https://doi.org/10.1007/s10664-013-9251-2

29.

Peterson’s algorithm, May 17. https://en.wikipedia.org/wiki/Peterson

30.

Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115–116 (1981). https://doi.org/10.1016/0020-0190(81)90106-XCrossRefMATH

31.

Wesselink, W., Willemse, T.A.C.: Evidence extraction from parameterised boolean equation systems. In: Benzmüller, C., Otten, J. (eds.) Proceedings of the 3rd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2018) affiliated with the International Joint Conference on Automated Reasoning (IJCAR 2018), Oxford, UK, July 18, 2018. CEUR Workshop Proceedings, vol. 2095, pp. 86–100. CEUR-WS.org (2018). http://ceur-ws.org/Vol-2095/paper6.pdf

Titel: Tutorial: Designing Distributed Software in mCRL2
verfasst von: Jan Friso Groote
Jeroen J. A. Keiren
Verlag: Springer International Publishing
Buch: Formal Techniques for Distributed Objects, Components, and Systems
Print ISBN: 978-3-030-78088-3

Electronic ISBN: 978-3-030-78089-0

Copyright-Jahr: 2021
DOI: https://doi.org/10.1007/978-3-030-78089-0_15

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"