Difference between revisions of "MACS PSI 2015"
From CERES
| (7 intermediate revisions by one user not shown) | |||
| Line 1: | Line 1: | ||
| + | = Modeling and Analysis of Concurrent Systems = | ||
| + | |||
| + | |||
| + | ==Tutorial Description== | ||
| + | This is half-a-day tutorial held at the [http://psi.university.innopolis.ru/ PSI 2015] conference at Innopolis, Russia. . | ||
| + | |||
| + | It gives an overview on the book | ||
| + | [http://mitpress.mit.edu/books/modeling-and-analysis-communicating-systems 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 [http://www.mcrl2.org/ mCRL2 toolset], which is freely | ||
| + | available under the Boost license. | ||
| + | |||
| + | |||
| + | |||
| + | ==Lecturer== | ||
| + | [[Mohammad Mousavi]] | ||
| + | |||
| + | * Office: E 305 | ||
| + | * Telephone 035 16 71 22 | ||
| + | * Email: [m.r.mousavi@hh.se] | ||
{| class="wikitable" | {| class="wikitable" | ||
| Line 20: | Line 46: | ||
|| | || | ||
| − | [https://www.kaltura.com/index.php/extwidget/openGraph/wid/0_e0fpcp7q - Video Part I] | + | [https://www.kaltura.com/index.php/extwidget/openGraph/wid/0_e0fpcp7q Trace Equiv. - Video Part I] |
| − | [https://www.kaltura.com/index.php/extwidget/openGraph/wid/0_t22d77rf - Video Part II] | + | [https://www.kaltura.com/index.php/extwidget/openGraph/wid/0_t22d77rf Bisimulation - Video Part II] |
| − | [https://www.kaltura.com/index.php/extwidget/openGraph/wid/0_gaobixvl - Video Part III] | + | [https://www.kaltura.com/index.php/extwidget/openGraph/wid/0_gaobixvl Weak Equiv. - Video Part III] |
|- | |- | ||
| Line 42: | Line 68: | ||
[https://www.kaltura.com/index.php/extwidget/openGraph/wid/0_dtf7z6bv HML - Video Part II] | [https://www.kaltura.com/index.php/extwidget/openGraph/wid/0_dtf7z6bv HML - Video Part II] | ||
| − | [https://www.kaltura.com/index.php/extwidget/openGraph/wid/0_2l0fv4qt - Video Part III] | + | [https://www.kaltura.com/index.php/extwidget/openGraph/wid/0_2l0fv4qt Modal mu-Calc. - Video Part III] |
| − | [https://www.kaltura.com/index.php/extwidget/openGraph/wid/0_k4s0e6co - Video Part IV] | + | [https://www.kaltura.com/index.php/extwidget/openGraph/wid/0_k4s0e6co Modal mu-Calc. - Video Part IV] |
|- | |- | ||
| Line 57: | 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]] | ||
|} | |} | ||
| − | [ | + | [https://ocw.tudelft.nl/courses/system-validation/ System Validation at Delft Opencourseware] |
| + | |||
| + | |||
| + | =[[Mohammad Mousavi|Back to Home]]= | ||
Latest revision as of 07:06, 4 May 2017
Contents
[hide]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
