Atif M., Groote J.F. Understanding Behaviour of Distributed Systems Using mCRL2

Springer, 2023. — 241 p.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 behavior of distributed systems, in particular where there is concurrency with inter-process communication. This language allows us to analyze a distributed system concerning 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 modeling tips and tricks.Understanding a distributed system’s behavior 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 behavior of communicating systems and generate, reduce, and visualize it as labeled transition systems. We also show how to do model-checking, which allows checking properties on the behavior, such as whether the behavior 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 eyebrows high as the results are often surprising. Using counter-examples can reveal behavior 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 behavior 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 specialized 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 analyze the behavior of distributed systems and protocols. It can easily express non-computable behavioral 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 analyzing 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 modeling 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 behavior 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), an e-Tag system for road tax collection, e-Commerce systems, or other systems having communication 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 behavior of a system is modeled 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 analyzing system behavior. The targeted systems for such an analysis are those systems having concurrent processes with inter-process communication. In this book, we study system modeling and model-checking techniques. Interestingly, model-checking provides beneficial results, but at the same time, it poses particular challenges as well. Formulating behavior precisely, especially formalizing properties that the behavior must have, is not always easy. Not only it is hard to understand the behavior 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 modeled system may become so complex that the tools can no longer analyze 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 to apply model-checking effectively.Introducing mCRL.
Automata to Represent Behavior.
Communicating Processes.
Behavioral Equivalences.
Data Types and Data-Dependent Behavior.
Model-Checking.
. The Modal -Calculus.
Linear Processes and Parameterised BESs.
Applications: Puzzles and Games.
Applications: Distributed Algorithms.