Course at RIO 2023 Summer School of Informatics
Rio Cuarto, Argentina; February 13-17, 2023
Overview
The aim of this course is to provide a basic understanding of modelling formalisms for concurrent systems. It will follow the so-called interleaving approach, which reduces the phenomenon of concurrency to a non-deterministic merging of sequential executions of sub-processes. This method is represented by Milner’s Calculus of Communicating Systems, a process algebra which provides a mathematical basis for describing both the structure and the behaviour of systems in a compositional way. To support formal reasoning about their correctness properties, we will introduce behavioural equivalences and logic-based techniques, and will demonstrate their tool-based application on mutual-exclusion algorithms.
Contents
- Milner’s Calculus of Communicating Systems
- Behavioural Equivalences
- Logical Specifications
- Application to Mutual-Exclusion Protocols
Exam
The exam is organised in the form of a homework task, in which you have to model a simple data communication protocol. Details are given in this document. The corresponding report has to be submitted to rio2023@i2.informatik.rwth-aachen.de by March 31, 2023.
Additional Material
- Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen and Jiri Srba: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, 2007.
- A draft version of the first part is available here.
- Check out the CAAL Tool developed at Aalborg University, which is used in the exercises and lectures.
- The CAAL specifications from the lectures can be found here.