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.
Author(s): Muhammad Atif, Jan Friso Groote
Series: Studies in Systems, Decision and Control, 458
Publisher: Springer
Year: 2023
Language: English
Pages: 240
City: Cham
Preface
Acknowledgments
Introduction
Welcome
Who Is This Book For?
What Is Covered in This Book?
Your Feedback and Errata
Contents
1 Introducing mCRL2
1.1 What is mCRL2 All About?
1.2 History of mCRL2
1.3 Why mCRL2?
1.4 Learning mCRL2
1.5 Other Educational Material
1.6 The mCRL2 Toolkit
1.7 Other Toolsets
2 Automata to Represent Behaviour
2.1 Why Make Models?
2.2 Developing Models in mCRL2
2.2.1 Hello-World Example
2.2.2 Using the Terminal
2.2.3 State-Space and Actions
2.3 Using the GUI
3 Communicating Processes
3.1 Communication Among Actions
3.1.1 A Coffee Vending Machine
3.2 Deadlock
3.3 Synchronous Versus Asynchronous Communication
3.4 Blocking and Renaming Actions
3.5 Hiding Actions
4 Behavioural Equivalences
4.1 Trace Equivalence
4.1.1 Weak Trace Equivalence
4.2 Strong Bisimulation
4.3 Branching Bisimulation
4.4 Divergence Preserving Branching Bisimulation
5 Data Types and Data-Dependent Behaviour
5.1 Sending/Receiving Data
5.1.1 Operators on Data
5.2 Conditions
5.3 Data Structures
5.3.1 Lists
5.3.2 Sets
5.3.3 Bags
5.4 User Defined Functions
5.4.1 Defining Constants
5.4.2 λ-Expressions
5.5 Constructors of a Data Type
5.6 Defining a Struct Data Type
5.7 Modelling the Alternating Bit Protocol
5.8 Modelling Milner's Cyclic Scheduler
6 Model-Checking
6.1 Hennessy-Milner Logic
6.2 Model-Checking with mCRL2
6.2.1 Parameterised Boolean Equation System
6.3 Action Formulas
6.4 Regular Formulas
6.5 Formulas with Data and Quantifiers
6.6 What to do if Model-Checking Becomes Time Consuming?
6.6.1 Reduce the Problem Size
6.6.2 Optimising and Transforming a PBES
6.6.3 Model-Check Explicit State Spaces
6.6.4 CADP
6.6.5 LTSmin and Pbessolvesymbolic
7 The Modal µ-Calculus
7.1 Minimal Fixed Points
7.1.1 Minimal Fixed Point Formulas with Data
7.2 Maximal Fixed Points
7.2.1 Maximal Fixed Points with Data
7.3 Combining Minimal and Maximal Fixed Points
7.4 Modelling a Movable Patient Support Unit and Its Requirements
7.4.1 Formal Specification
7.4.2 Requirements Analysis
8 Linear Processes and Parameterised BESs
8.1 Linear Processes
8.2 Optimising an LPS
8.2.1 Rewriting a Linear Process
8.2.2 Constant Elimination
8.2.3 Parameter Elimination
8.2.4 Sum Instantiation and Sum Elimination
8.2.5 Action Renaming
8.2.6 Unfolding Parameters
8.3 Parameterised Boolean Equation Systems
8.4 Optimising PBESs
8.4.1 Rewriting PBESs
8.4.2 Constant Elimination
8.4.3 Parameter Elimination
9 Applications: Puzzles and Games
9.1 Magic Square
9.2 Bridge Crossing
9.3 Weight Bars Crossing
9.4 The Wolf, the Goat and Cabbage
9.5 Jumping Frogs
9.6 Tic-Tac-Toe
10 Applications: Distributed Algorithms
10.1 Heartbeat Protocols
10.2 The Binary Heartbeat Protocol
10.3 The Static Heartbeat Protocol
10.4 The Expanding and the Dynamic Heartbeat Protocol
Appendix A Specifications of Protocols in mCRL2
A.1 Binary Heartbeat Protocol
A.2 Static Heartbeat Protocol
Appendix B Solutions
Appendix References
Index
