Tutorial: Designing Distributed Software in mCRL2

Jan Friso Groote; Jeroen J. A. Keiren

doi:10.1007/978-3-030-78089-0_15

Tutorial: Designing Distributed Software in mCRL2

Jan Friso Groote, Jeroen J. A. Keiren

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

7 Citations (Scopus)

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.

Original language	English
Title of host publication	Formal Techniques for Distributed Objects, Components, and Systems - 41st IFIP WG 6.1 International Conference, FORTE 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Proceedings
Editors	Kirstin Peters, Tim A. Willemse
Publisher	Springer
Pages	226-243
Number of pages	18
ISBN (Print)	9783030780883
DOIs	https://doi.org/10.1007/978-3-030-78089-0_15
Publication status	Published - 2021
Event	41st IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2021 held as part of 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021 - Virtual, Online Duration: 14 Jun 2021 → 18 Jun 2021

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	12719 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	41st IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2021 held as part of 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021
City	Virtual, Online
Period	14/06/21 → 18/06/21

Bibliographical note

Publisher Copyright:
© 2021, IFIP International Federation for Information Processing.

Keywords

Counterexamples
Distributed software
mCRL2 toolset
Model checking
Parallel software

Access to Document

10.1007/978-3-030-78089-0_15

Cite this

Groote, J. F., & Keiren, J. J. A. (2021). Tutorial: Designing Distributed Software in mCRL2. In K. Peters, & T. A. Willemse (Eds.), Formal Techniques for Distributed Objects, Components, and Systems - 41st IFIP WG 6.1 International Conference, FORTE 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Proceedings (pp. 226-243). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12719 LNCS). Springer. https://doi.org/10.1007/978-3-030-78089-0_15

Groote, Jan Friso ; Keiren, Jeroen J. A. / Tutorial : Designing Distributed Software in mCRL2. Formal Techniques for Distributed Objects, Components, and Systems - 41st IFIP WG 6.1 International Conference, FORTE 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Proceedings. editor / Kirstin Peters ; Tim A. Willemse. Springer, 2021. pp. 226-243 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{e54eaee9d61a4b16ba2a9615e328abcf,

title = "Tutorial: Designing Distributed Software in mCRL2",

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.",

keywords = "Counterexamples, Distributed software, mCRL2 toolset, Model checking, Parallel software",

author = "Groote, {Jan Friso} and Keiren, {Jeroen J. A.}",

note = "Publisher Copyright: {\textcopyright} 2021, IFIP International Federation for Information Processing.; 41st IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2021 held as part of 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021 ; Conference date: 14-06-2021 Through 18-06-2021",

year = "2021",

doi = "10.1007/978-3-030-78089-0_15",

language = "English",

isbn = "9783030780883",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "226--243",

editor = "Kirstin Peters and Willemse, {Tim A.}",

booktitle = "Formal Techniques for Distributed Objects, Components, and Systems - 41st IFIP WG 6.1 International Conference, FORTE 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Proceedings",

address = "Germany",

}

Groote, JF & Keiren, JJA 2021, Tutorial: Designing Distributed Software in mCRL2. in K Peters & TA Willemse (eds), Formal Techniques for Distributed Objects, Components, and Systems - 41st IFIP WG 6.1 International Conference, FORTE 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12719 LNCS, Springer, pp. 226-243, 41st IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2021 held as part of 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Virtual, Online, 14/06/21. https://doi.org/10.1007/978-3-030-78089-0_15

Tutorial: Designing Distributed Software in mCRL2. / Groote, Jan Friso ; Keiren, Jeroen J. A.
Formal Techniques for Distributed Objects, Components, and Systems - 41st IFIP WG 6.1 International Conference, FORTE 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Proceedings. ed. / Kirstin Peters; Tim A. Willemse. Springer, 2021. p. 226-243 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12719 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Tutorial

T2 - 41st IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2021 held as part of 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021

AU - Groote, Jan Friso

AU - Keiren, Jeroen J. A.

PY - 2021

Y1 - 2021

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

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

KW - Counterexamples

KW - Distributed software

KW - mCRL2 toolset

KW - Model checking

KW - Parallel software

UR - http://www.scopus.com/inward/record.url?scp=85111374217&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-78089-0_15

DO - 10.1007/978-3-030-78089-0_15

M3 - Conference contribution

AN - SCOPUS:85111374217

SN - 9783030780883

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 226

EP - 243

BT - Formal Techniques for Distributed Objects, Components, and Systems - 41st IFIP WG 6.1 International Conference, FORTE 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Proceedings

A2 - Peters, Kirstin

A2 - Willemse, Tim A.

PB - Springer

Y2 - 14 June 2021 through 18 June 2021

ER -

Groote JF , Keiren JJA. Tutorial: Designing Distributed Software in mCRL2. In Peters K, Willemse TA, editors, Formal Techniques for Distributed Objects, Components, and Systems - 41st IFIP WG 6.1 International Conference, FORTE 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Proceedings. Springer. 2021. p. 226-243. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-78089-0_15

Tutorial: Designing Distributed Software in mCRL2

Abstract

Publication series

Conference

Bibliographical note

Keywords

Access to Document

Other files and links

Fingerprint

Tutorial: Designing Distributed Software in mCRL2

Cite this