Tutorial: Designing Distributed Software in mCRL2
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , |
|---|---|
| Format: | Preprint |
| Publié: |
2021
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866916884395327488 |
|---|---|
| author | Groote, Jan Friso Keiren, Jeroen J. A. |
| author_facet | Groote, Jan Friso Keiren, Jeroen J. A. |
| contents | 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 (https://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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2104_10542 |
| institution | arXiv |
| publishDate | 2021 |
| record_format | arxiv |
| spellingShingle | Tutorial: Designing Distributed Software in mCRL2 Groote, Jan Friso Keiren, Jeroen J. A. Logic in Computer Science 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 (https://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. |
| title | Tutorial: Designing Distributed Software in mCRL2 |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2104.10542 |