MACS Ed 2014

From CERES
Jump to: navigation, search

Modeling and Analysis of Communicating Systems - Edition 2014

Contact

Lecturer

Mohammad Mousavi


Objectives

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

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


Slides and Study Material

Lecture Handouts / Slides Other Material
Lecture 1: Introduction Handouts Slides
Lecture 2: Behavrioal Specification Handouts Slides Adam's Slides on UPPAAL
Lecture 3: Temporal Logic Handouts Slides Nikita's Slides on the ETSI Standard for Inter-Vehicular Communiation
Lecture 4: Abstract Data Types and

SequentialProcesses

ADT Handouts ADT Slides

Seq. Proc. Handouts Seq. Proc. Slides

Books

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.