The assignment consists of designing a controller for a small embedded system. A description of a recommended assignment is posted below. However, it is possible to design any embedded controller or distributed algorithm provided you obtain approval by the lecturer. The assignment can be carried out in groups of three to four students.
N.B. The exam material comprises Chapters 1 to 6 (inclusive) of the course reader. Sections 2.3.3, 2.5.3, 3.3, 3.6 (printed version only), 5.4, 5.5, 6.2, 6.4 and 6.5 are not treated in the lectures and will not be part of the exam material. The topics treated in the course and included in the final exam are: actions, weak and strong behavioral equivalences, algebraic data types, sequential and parallel processes, modal mu-calculus and modeling system behavior.
| date | topics | slides | exercises |
|---|---|---|---|
| Lecture 1 September 6 (at StakOkay Arnhem) |
Introduction to Behavioral Specification Behavioral Equivalences |
Introduction Behavioral Equivalences: Part I |
2.3.7 |
| Lecture 2 September 13 |
Behavioral Equivalences | Behavioral Equivalences: Part II | 2.3.2, 2.3.7, 2.3.8, 2.3.9 |
| Lecture 3 September 20 |
Abstract Data Types | Abstract Data Types (proofs are now included in the slides) |
2.5.4, 2.5.5, 3.1.1, 3.1.2 |
| Lecture 4 September 27 |
Sequential Processes: Theory | Sequential Processes | 4.2.1-2, 4.3.1-2, 4.5.1-2 |
| Lecture 5 October 4 |
Sequential Processes: Reasoning and Examples | Coffee Machine Examples | |
| Lecture 6 October 11 |
Parallel Processes: Theory and Examples | Parallel Processes Two-Place Buffer Examples |
5.1.1-2, 5.2.1 |
| Lecture 7 October 18 |
Modal mu-Calculus | Modal mu-Calculus | 6.2.1, 6.3.1-6.3.2, 6.3.4 |
| Lecture 8 October 25 |
Model Exam | Assessment Guide | Model Exam Solutions |