MACS Ed 2014 - Revision history

Ceres at 06:27, 5 May 2017

2017-05-05T06:27:33Z

Ceres at 17:03, 4 March 2015

2015-03-04T17:03:50Z

Ceres at 08:10, 11 December 2014

2014-12-11T08:10:34Z

Ceres at 15:33, 19 November 2014

2014-11-19T15:33:04Z

Ceres at 14:50, 19 November 2014

2014-11-19T14:50:16Z

Ceres at 14:49, 19 November 2014

2014-11-19T14:49:35Z

Ceres at 06:04, 19 November 2014

2014-11-19T06:04:01Z

Ceres at 06:03, 19 November 2014

2014-11-19T06:03:40Z

Ceres: Created page with "= Modeling and Analysis of Communicating Systems - Edition 2014 = ==Contact == ===Lecturer=== Mohammad Mousavi * Office: E 305 * Telephone 035 16 71 22 * Email: [m...."

2014-11-18T10:36:59Z

Created page with "= Modeling and Analysis of Communicating Systems - Edition 2014 = ==Contact == ===Lecturer=== Mohammad Mousavi * Office: E 305 * Telephone 035 16 71 22 * Email: [m...."

New page

= Modeling and Analysis of Communicating Systems - Edition 2014 =

==Contact ==

===Lecturer===
[[Mohammad Mousavi]]

* 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 ==

{| class="wikitable"
|-
! Lecture !! Handouts / Slides !! Other Material
|-
| 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]] ||
|-
|}

← Older revision		Revision as of 06:27, 5 May 2017
Line 1:		Line 1:
−	= Modeling and Analysis of Communicating Systems ~~- Edition 2014~~ =	+	= Modeling and Analysis of Communicating Systems =

@@ Line 42: / Line 42: @@
 |-
 |  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]]
 |-
 |}

← Older revision		Revision as of 15:33, 19 November 2014
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.

@@ Line 9: / Line 9: @@
 * Office: E 305
 * Telephone 035 16 71 22
-* Email: [mailto:m.r.mousavi@hh.se]
+* Email: [mailto:m.r.mousavi@hh.se m.r.mousavi@hh.se]

@@ Line 40: / Line 40: @@
 |-
 |  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]]
 |-
 |}

@@ Line 39: / Line 39: @@
 |  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]]
 |-
 |}