MACS PSI 2015
Contents
Modeling and Analysis of Concurrent Systems
Tutorial Description
This is half-a-day tutorial held at the PSI 2015 conference at Innopolis, Russia. .
It gives an overview on the 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 system 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 book is to mathematically verify the correctness of communicating systems.
The theory is implemented in the mCRL2 toolset, which is freely available under the Boost license.
Lecturer
- Office: E 305
- Telephone 035 16 71 22
- Email: [m.r.mousavi@hh.se]
| Lecture | Handouts / Slides | Other Material |
|---|---|---|
| Lecture 1: Introduction | Introduction - Slides | |
| Lecture 2: Actions, Behavior, Abstraction | Behavioral Modeling - Slides | |
| Lecture 3: Behavioral Equivalences | Equivalences - Slides Part I | |
| Lecture 3: Hennessy Milner Logic | HML - Slides Part I | |
| Lecture 4: Sequential Processes | Sequential Processes - Slides Part I | |
| Lecture 5: Parallel Processes | Parallel Processes - Slides |
System Validation at Delft Opencourseware
