Revision as of 16:33, 19 November 2014

Modeling and Analysis of Communicating Systems - Edition 2014

On completion of the course students will be able to

Know concept of behavioural specification (Knowledge)
Know concept of behavioural equivalence (Knowledge)
Know how to specify logical properties (in temporal logics and modal mu-calculus) (Knowledge)

Manually reason about simple systems (both equationally, and using the semantics of logics) (Application)

Specify the behaviour of embedded systems or communication protocols (Application)
Verify specification satisfies its requirements (Application)

Assessment is performed in terms of a short paper and a practical project.

Lecture	Handouts / Slides	Other Material
Lecture 1: Introduction	Handouts Slides
Lecture 2: Behavrioal Specification	Handouts Slides	Adam's Slides on UPPAAL

M.R. Mousavi and J.F. Groote. Modeling and Analysis of Communicating Systems, MIT Press, 2014

C. Baier and J.P. Katoen. Principles of Model Checking, MIT Press, 2008.

L. Aceto, A. Ingolfsdottir, K.G. Larsen, and J. Srba. Reactive Systems: Modelling, Specification and Verification, Cambridge University Press, 2010.

@@ Line 42: / Line 42: @@
 |-
 |}
+=== Books ===
+M.R. Mousavi and J.F. Groote. [http://mitpress.mit.edu/books/modeling-and-analysis-communicating-systems Modeling and Analysis of Communicating Systems], MIT Press, 2014
+C. Baier and J.P. Katoen. [http://mitpress.mit.edu/books/principles-model-checking Principles of Model Checking], MIT Press, 2008.
+L. Aceto, A. Ingolfsdottir, K.G. Larsen, and J. Srba. [http://www.cambridge.org/us/academic/subjects/computer-science/programming-languages-and-applied-logic/reactive-systems-modelling-specification-and-verification Reactive Systems: Modelling, Specification and Verification], Cambridge University Press, 2010.