Difference between revisions of "MACS PSI 2015"
| Line 83: | Line 83: | ||
[https://www.kaltura.com/index.php/extwidget/openGraph/wid/0_pdhhy802 Sequential Processes - Video Part II] | [https://www.kaltura.com/index.php/extwidget/openGraph/wid/0_pdhhy802 Sequential Processes - Video Part II] | ||
| + | |||
| + | |- | ||
| + | | Lecture 5: Parallel Processes | ||
| + | |||
| + | || | ||
| + | |||
| + | || [[media:MACS_PSI_ParProc.pdf| Parallel Processes - Slides ]] | ||
| + | |||
| + | || | ||
| + | [https://www.kaltura.com/index.php/extwidget/openGraph/wid/0_0tqad0w2 Parallel Processes - Video]] | ||
|} | |} | ||
[http://ocw.tudelft.nl/courses/computerscience/systemvalidation/course-home/ System Validation at Delft Opencourseware] | [http://ocw.tudelft.nl/courses/computerscience/systemvalidation/course-home/ System Validation at Delft Opencourseware] | ||
Revision as of 13:03, 5 November 2015
Modeling and Analysis of Concurrent Systems
Tutorial Description
This is half-a-day tutorial held at the PSI 2015 conference at Innapolis, 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 |
