Difference between revisions of "MACS PSI 2015"

From CERES
Jump to: navigation, search
 
(12 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 11: Line 37:
 
||    [[media:MACS_PSI_behavior.pdf| Behavioral Modeling - Slides]]    ||  
 
||    [[media:MACS_PSI_behavior.pdf| Behavioral Modeling - Slides]]    ||  
 
[https://www.kaltura.com/index.php/extwidget/openGraph/wid/0_75li7l0k Behavioral Modeling -  Video]
 
[https://www.kaltura.com/index.php/extwidget/openGraph/wid/0_75li7l0k Behavioral Modeling -  Video]
 +
|-
 +
|  Lecture 3: Behavioral Equivalences
 +
||    [[media:MACS_PSI_Eq_1.pdf| Equivalences - Slides Part I]]   
 +
 +
[[media:MACS_PSI_Eq_2.pdf| Equivalences - Slides Part II]]   
 +
 +
[[media:MACS_PSI_Eq_3.pdf| Equivalences - Slides Part III]]   
 +
||
 +
 +
[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  Bisimulation -  Video Part II]
 +
 +
[https://www.kaltura.com/index.php/extwidget/openGraph/wid/0_gaobixvl  Weak Equiv. -  Video Part III]
 +
 
|-
 
|-
 
|  Lecture 3: Hennessy Milner Logic
 
|  Lecture 3: Hennessy Milner Logic
Line 27: 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 Modal mu-Calc. -  Video Part III]
 +
 +
[https://www.kaltura.com/index.php/extwidget/openGraph/wid/0_k4s0e6co Modal mu-Calc. -  Video Part IV]
 +
 +
|-
 +
|  Lecture 4: Sequential Processes
 +
||    [[media:MACS_PSI_SeqProc_1.pdf| Sequential Processes - Slides Part I]]   
 +
 +
[[media:MACS_PSI_SeqProc_2.pdf| Sequential Processes - Slides Part II]]
 +
 +
||
 +
 +
[https://www.kaltura.com/index.php/extwidget/openGraph/wid/0_yldxww8z Sequential Processes  -  Video Part I]
 +
 +
[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

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

Mohammad Mousavi

  • Office: E 305
  • Telephone 035 16 71 22
  • Email: [m.r.mousavi@hh.se]
Lecture Handouts / Slides Other Material
Lecture 1: Introduction Introduction - Slides

Introduction - Video

Lecture 2: Actions, Behavior, Abstraction Behavioral Modeling - Slides

Behavioral Modeling - Video

Lecture 3: Behavioral Equivalences Equivalences - Slides Part I

Equivalences - Slides Part II

Equivalences - Slides Part III

Trace Equiv. - Video Part I

Bisimulation - Video Part II

Weak Equiv. - Video Part III

Lecture 3: Hennessy Milner Logic HML - Slides Part I

HML - Slides Part II

HML - Slides Part III

HML - Slides Part IV

HML - Video Part I

HML - Video Part II

Modal mu-Calc. - Video Part III

Modal mu-Calc. - Video Part IV

Lecture 4: Sequential Processes Sequential Processes - Slides Part I

Sequential Processes - Slides Part II

Sequential Processes - Video Part I

Sequential Processes - Video Part II

Lecture 5: Parallel Processes Parallel Processes - Slides

Parallel Processes - Video]

System Validation at Delft Opencourseware


Back to Home

Retrieved from "https://wiki.hh.se/ceres/index.php?title=MACS_PSI_2015&oldid=6655"