{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T09:48:29Z","timestamp":1766137709161,"version":"3.41.0"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030780883"},{"type":"electronic","value":"9783030780890"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-78089-0_15","type":"book-chapter","created":{"date-parts":[[2021,6,9]],"date-time":"2021-06-09T14:26:35Z","timestamp":1623248795000},"page":"226-243","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Tutorial: Designing Distributed Software in mCRL2"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2196-6587","authenticated-orcid":false,"given":"Jan Friso","family":"Groote","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5772-9527","authenticated-orcid":false,"given":"Jeroen J. A.","family":"Keiren","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,6,8]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Apt, K.R., Olderog, E.: Fifty years of Hoare\u2019s logic. Formal Aspects Comput. 31(6), 751\u2013807 (2019). https:\/\/doi.org\/10.1007\/s00165-019-00501-3","DOI":"10.1007\/s00165-019-00501-3"},{"key":"15_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-13345-3_7","volume-title":"Automata, Languages and Programming","author":"JA Bergstra","year":"1984","unstructured":"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\u201394. Springer, Heidelberg (1984). https:\/\/doi.org\/10.1007\/3-540-13345-3_7"},{"key":"15_CR3","doi-asserted-by":"publisher","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development - Coq\u2019Art: 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","DOI":"10.1007\/978-3-662-07964-5"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-319-67113-0_14","volume-title":"Critical Systems: Formal Methods and Automated Verification","author":"R van Beusekom","year":"2017","unstructured":"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\u2013233. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-67113-0_14"},{"key":"15_CR5","doi-asserted-by":"publisher","unstructured":"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\u201350 (2020). https:\/\/doi.org\/10.4204\/EPTCS.322.5","DOI":"10.4204\/EPTCS.322.5"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Bouwman, M., Luttik, B., Willemse, T.A.C.: Off-the-shelf automated analysis of liveness properties for just paths. Acta Informatica 57(3\u20135), 551\u2013590 (2020). https:\/\/doi.org\/10.1007\/s00236-020-00371-w","DOI":"10.1007\/s00236-020-00371-w"},{"key":"15_CR7","doi-asserted-by":"publisher","unstructured":"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\u2013756. North-Holland (2007). https:\/\/doi.org\/10.1016\/s1570-2464(07)80015-2","DOI":"10.1016\/s1570-2464(07)80015-2"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"van den Brand, M., Groote, J.F.: Software engineering: redundancy is key. Sci. Comput. Program. 97, 75\u201381 (2015). https:\/\/doi.org\/10.1016\/j.scico.2013.11.020","DOI":"10.1016\/j.scico.2013.11.020"},{"key":"15_CR9","series-title":"Advances in Intelligent Systems and Computing","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-319-33622-0_19","volume-title":"Software Engineering Perspectives and Application in Intelligent Systems","author":"F Cicirelli","year":"2016","unstructured":"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\u2013215. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33622-0_19"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"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\u20133139 (2011). https:\/\/doi.org\/10.1016\/j.tcs.2011.02.034","DOI":"10.1016\/j.tcs.2011.02.034"},{"issue":"9","key":"15_CR11","doi-asserted-by":"publisher","first-page":"569","DOI":"10.1145\/365559.365617","volume":"8","author":"EW Dijkstra","year":"1965","unstructured":"Dijkstra, E.W.: Solution of a problem in concurrent programming control. Commun. ACM 8(9), 569 (1965). https:\/\/doi.org\/10.1145\/365559.365617","journal-title":"Commun. ACM"},{"key":"15_CR12","unstructured":"Dijkstra, E.W.: Over de sequentialiteit van procesbeschrijvingen (Undated, 1962 or 1963)"},{"key":"15_CR13","doi-asserted-by":"publisher","unstructured":"Dyseryn, V., van Glabbeek, R.J., H\u00f6fner, 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\u201334 (2017). https:\/\/doi.org\/10.4204\/EPTCS.255.2","DOI":"10.4204\/EPTCS.255.2"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"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\u2013107 (2013). https:\/\/doi.org\/10.1007\/s10009-012-0244-z","DOI":"10.1007\/s10009-012-0244-z"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"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\u2013167 (2016). https:\/\/doi.org\/10.1007\/s10009-015-0377-y","DOI":"10.1007\/s10009-015-0377-y"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-030-40914-2_2","volume-title":"Formal Aspects of Component Software","author":"JF Groote","year":"2020","unstructured":"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\u201348. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-40914-2_2"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"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\u201333 (2015). https:\/\/doi.org\/10.1002\/stvr.1536","DOI":"10.1002\/stvr.1536"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.7551\/mitpress\/9946.001.0001"},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-319-68270-9_3","volume-title":"ModelEd, TestEd, TrustEd","author":"JF Groote","year":"2017","unstructured":"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\u201363. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68270-9_3"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Groote, J.F., Wiedijk, F., Zantema, H.: A probabilistic analysis of the game of the goose. SIAM Rev. 58(1), 143\u2013155 (2016). https:\/\/doi.org\/10.1137\/140983781","DOI":"10.1137\/140983781"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.23638\/LMCS-16(3:19)2020"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137\u2013161 (1985). https:\/\/doi.org\/10.1145\/2455.2460","DOI":"10.1145\/2455.2460"},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"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\u2013144 (2005). https:\/\/doi.org\/10.1016\/j.entcs.2005.04.008","DOI":"10.1016\/j.entcs.2005.04.008"},{"key":"15_CR24","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M., W\u00fcstholz, V.: The Dafny integrated development environment. In: Dubois, C., Giannakopoulou, D., M\u00e9ry, D. (eds.) Proceedings 1st Workshop on Formal Integrated Development Environment, F-IDE 2014, Grenoble, France, 6 April 2014. EPTCS, vol. 149, pp. 3\u201315 (2014). https:\/\/doi.org\/10.4204\/EPTCS.149.2","DOI":"10.4204\/EPTCS.149.2"},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"Mateescu, R., Serwe, W.: Model checking and performance evaluation with CADP illustrated on shared-memory mutual exclusion protocols. Sci. Comput. Program. 78(7), 843\u2013861 (2013). https:\/\/doi.org\/10.1016\/j.scico.2012.01.003","DOI":"10.1016\/j.scico.2012.01.003"},{"key":"15_CR26","unstructured":"Milner, R.: Communication and concurrency. PHI Series in Computer Science. Prentice Hall, Upper Saddle River (1989)"},{"key":"15_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"15_CR28","doi-asserted-by":"crossref","unstructured":"Osaiweran, A., Schuts, M., Hooman, J.: Experiences with incorporating formal techniques into industrial practice. Empir. Softw. Eng. 19(4), 1169\u20131194 (2014). https:\/\/doi.org\/10.1007\/s10664-013-9251-2","DOI":"10.1007\/s10664-013-9251-2"},{"key":"15_CR29","unstructured":"Peterson\u2019s algorithm, May 17. https:\/\/en.wikipedia.org\/wiki\/Peterson"},{"issue":"3","key":"15_CR30","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0020-0190(81)90106-X","volume":"12","author":"GL Peterson","year":"1981","unstructured":"Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115\u2013116 (1981). https:\/\/doi.org\/10.1016\/0020-0190(81)90106-X","journal-title":"Inf. Process. Lett."},{"key":"15_CR31","unstructured":"Wesselink, W., Willemse, T.A.C.: Evidence extraction from parameterised boolean equation systems. In: Benzm\u00fcller, 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\u2013100. CEUR-WS.org (2018). http:\/\/ceur-ws.org\/Vol-2095\/paper6.pdf"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Distributed Objects, Components, and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-78089-0_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,8]],"date-time":"2025-06-08T22:04:09Z","timestamp":1749420249000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-78089-0_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030780883","9783030780890"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-78089-0_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"8 June 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FORTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Techniques for Distributed Objects, Components, and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Valletta","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Malta","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 June 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 June 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"41","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"forte2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.discotec.org\/2021\/forte","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"35% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Due to the Corona pandemic this event was held virtually.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}