ABSTRACT. This half day tutorial addresses the issue of formal modeling and verification of distributed and concurrent systems based on the recent book Modeling and Analysis of Communicating Systems that appeared in the summer of 2014. The theory in the book is developed with as major guideline how to model and verify real life behaviour. It rests on two pillars, namely process algebras for behavioural description and modal logic to characterise requirements. As data is indispensable when describing realistic systems, both formalisms are endowed with a whole range of data types, including functions, sets and reals. Timed behaviour can also be expressed in both the algebra and the logic.

An important purpose of the tutorial is to give an overview of the techniques addressed in the book to mathematically verify the correctness of communicating systems. There are two major approaches. The first one is by proving that an implementation behaves the same (in the sense of e.g. branching bisimulation) to the specification. For these normal forms, tau-confluence and especially the Cones and Foci method are indispensible. The second one is to verify that modal formulas are valid for given processes, for which parameterised boolean equation systems are essential.

The theory is implemented in the mCRL2 toolset, which is freely available under the extremely liberal Boost license. This toolset can be used to prove behavioural equivalences, check the validity of modal formulas, visualise behaviour in various ways, and of course also to do normal matters such as simulating behaviour and generating or reducing state spaces. The toolset has been used to design and analyse a plethora of applications, including control systems at CERN. Experience shows that the quality of programs developed using such tools goes up ten-fold