Название: Understanding Behaviour of Distributed Systems Using mCRL2
Автор: Muhammad Atif, Jan Friso Groote
Издательство: Springer
Год: 2023
Страниц: 241
Язык: английский
Формат: pdf (true), epub
Размер: 27.6 MB

This book helps readers easily learn basic model checking by presenting examples, exercises and case studies. The toolset mCRL2 provides a language to specify the behaviour of distributed systems, in particular where there is concurrency with inter-process communication. This language allows us to analyse a distributed system with respect to its functional requirements. For example, biological cells, supply chain management systems, patient support platforms, and communication protocols. The underlying technique is based on verifying requirements through model checking. The book explains the syntax of mCRL2 and offers modelling tips and tricks.

Understanding a distributed system’s behaviour means getting insight into whether the system meets its expectations. Giving such a surety is challenging, primarily when a system consists of multiple participants. These participants can interact with each other in far more ways than we can imagine.

In this book, we explain how to model the behaviour of communicating systems and generate, reduce and visualise it as a labelled transition system. We also show how to do model-checking, which allows checking properties on the behaviour, such as whether the behaviour is free of deadlocks. Nevertheless, as we use the modal mu-calculus with data, virtually any conceivable safety, liveness and fairness property can be formulated and checked. Applying model-checking makes everyone’s eyebrow high as the results are often surprising. Using counter-examples can reveal behaviour in distributed systems that no one, including the developers, deemed possible, and as such, it is an invaluable tool to obtain essential insight into the behaviour of modern programmed systems.

It is a general perception that model-checking has a steep learning curve. In this book, we try to mitigate this by introducing all concepts with small examples and thoroughly explaining system specifications line by line. We use mCRL2 (micro Common Representation Language 2) and the modal mu-calculus, which are specialised languages that specify a distributed system and formulate system properties. These languages come with an effective toolset, which is open source and can be freely used. mCRL2 is a very concise and, at the same time, extremely expressive language to specify and analyse the behaviour of distributed systems and protocols. It can easily express non-computable behavioural specifications and requirements. It goes without saying that for such descriptions, tool-supported analysis is not very fruitful. However, this implies that effectively using mCRL2 requires a good understanding of the language and formula writing in the mu-calculus.

This book is introductory and comprises subjects from installing the toolset mCRL2 to analysing simple systems. We start with writing hello world type systems and gradually increase the complexity of examples and exercises. So, anyone having some knowledge of computer programming, logic and basic mathematics can study this book and will learn how to model-check communication protocols, distributed algorithms and interacting systems. We focus to explain every topic with sufficient examples and exercises. A chapter on modelling and solving puzzles and another chapter on how to model heartbeat protocols illustrate the techniques.

This book intends to create an interest to reason about the correctness of the behaviour of programmed systems. There are a lot of such systems around us and available in the literature that needs to be studied and corrected. For example, we can study the protocol of an ATM (automated teller machine), e-Tag system for road tax collection, e-Commerce systems or other systems having communicating processes. It can be surprising to know that many of the existing distributed algorithms used in such systems are not completely correct, which can effectively be found by formal verification. In model-checking, the complete behaviour of a system is modelled and then searched exhaustively.

What Is Covered in This Book?
Features of mCRL2 are covered so that a reader can start from elementary and small examples to learn how to make models and check them.

Who Is This Book For?
This book is for those who want to use mCRL2 for automatically analysing system behaviour. The targeted systems for such an analysis are those systems having concurrent processes with inter-process communication. In this book, we study system modelling and model-checking techniques. Interestingly, model-checking provides beneficial results, but at the same time, it poses particular challenges as well. Formulating behaviour precisely, especially formalising properties that the behaviour must have, is not always easy. Not only it is hard to understand the behaviour and requirements, often given in ambiguous natural language, but correctly encoding them using minimal or maximal fixed point modalities requires some training and experience. Besides that, a modelled system may become so complex that the tools can no longer analyse it. This phenomenon is often referred to as the state space explosion problem. In this book, we study these challenges and the methods to address those challenges in order to apply model-checking effectively.

Contents:
1. Introducing mCRL2
2. Automata to Represent Behaviour
3. Communicating Processes
4. Behavioural Equivalences
5. Data Types and Data-Dependent Behaviour
6. Model-Checking
7. The Modal -Calculus
8. Linear Processes and Parameterised BESs
9. Applications: Puzzles and Games
10. Applications: Distributed Algorithms