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

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › Academic › peer review

7 Citaten (Scopus)

Samenvatting

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.

Originele taal-2	Engels
Titel	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
Redacteuren	Kirstin Peters, Tim A. Willemse
Uitgeverij	Springer
Pagina's	226-243
Aantal pagina's	18
ISBN van geprinte versie	9783030780883
DOI's	https://doi.org/10.1007/978-3-030-78089-0_15
Status	Gepubliceerd - 2021
Evenement	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 Duur: 14 jun. 2021 → 18 jun. 2021

Publicatie series

Naam	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	12719 LNCS
ISSN van geprinte versie	0302-9743
ISSN van elektronische versie	1611-3349

Congres

Congres	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
Stad	Virtual, Online
Periode	14/06/21 → 18/06/21

Bibliografische nota

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

Toegang tot document

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

Andere bestanden en links

Link naar publicatie in Scopus

7 Citaties
1 Preprint

Tutorial: Designing Distributed Software in mCRL2
Groote, J. F. & Keiren, J. J. A., 2021, (CoRR).
Onderzoeksoutput: Werkdocument › Preprint › Academic

Citeer dit

Groote, J. F., & Keiren, J. J. A. (2021). Tutorial: Designing Distributed Software in mCRL2. In K. Peters, & T. A. Willemse (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 (blz. 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. redacteur / Kirstin Peters ; Tim A. Willemse. Springer, 2021. blz. 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 (uitgave), 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, blz. 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. uitgave / Kirstin Peters; Tim A. Willemse. Springer, 2021. blz. 226-243 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12719 LNCS).

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › 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, redacteurs, 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. blz. 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

Samenvatting

Publicatie series

Congres

Bibliografische nota

Toegang tot document

Andere bestanden en links

Vingerafdruk

Onderzoekersoutput

Tutorial: Designing Distributed Software in mCRL2

Citeer dit