Difference between revisions of "MACS Ed 2014"
From CERES
| (4 intermediate revisions by one user not shown) | |||
| Line 1: | Line 1: | ||
| − | = Modeling and Analysis of Communicating Systems | + | = Modeling and Analysis of Communicating Systems = |
| Line 39: | Line 39: | ||
| Lecture 1: Introduction || [[media:macs_lecture1_handouts_2014.pdf| Handouts]] [[media:macs_lecture1_slides_2014.pdf| Slides]] || | | Lecture 1: Introduction || [[media:macs_lecture1_handouts_2014.pdf| Handouts]] [[media:macs_lecture1_slides_2014.pdf| Slides]] || | ||
|- | |- | ||
| − | | Lecture 2: Behavrioal Specification || [[media:macs_lecture2_handouts_2014.pdf| Handouts]] [[media:macs_lecture2_slides_2014.pdf| Slides]] || [[media:Adam's Slides on UPPAAL]] | + | | Lecture 2: Behavrioal Specification || [[media:macs_lecture2_handouts_2014.pdf| Handouts]] [[media:macs_lecture2_slides_2014.pdf| Slides]] || [[media:macs_adam_uppaal_slides_2014.pdf|Adam's Slides on UPPAAL]] |
| + | |- | ||
| + | | Lecture 3: Temporal Logic || [[media:macs_lecture3_handouts_2014.pdf| Handouts]] [[media:macs_lecture3_slides_2014.pdf| Slides]] || [[media:macs_nikita_dcc_mac_slides_2014.pdf|Nikita's Slides on the ETSI Standard for Inter-Vehicular Communiation]] | ||
| + | |- | ||
| + | | Lecture 4: Abstract Data Types and | ||
| + | |||
| + | SequentialProcesses | ||
| + | || | ||
| + | |||
| + | [[media:macs_lecture4_handouts_2015.pdf| ADT Handouts]] [[media:macs_lecture4_slides_2015.pdf| ADT Slides]] | ||
| + | |||
| + | [[media:macs_lecture5_handouts_2015.pdf| Seq. Proc. Handouts]] [[media:macs_lecture5_slides_2015.pdf| Seq. Proc. Slides]] | ||
| + | || | ||
|- | |- | ||
|} | |} | ||
| + | |||
| + | === 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. | ||
Latest revision as of 07:27, 5 May 2017
Contents
Modeling and Analysis of Communicating Systems
Contact
Lecturer
- Office: E 305
- Telephone 035 16 71 22
- Email: m.r.mousavi@hh.se
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 |
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.
