3TU Masters Program in Embedded Systems TU Delft
The purpose of this course is to learn how to specify the behaviour of embedded systems and to experience the design of a provably correct system. In this course you will learn how to formally specify requirements and to prove (or disprove) them on the behaviour. With a practical assignment you will experience how to apply the techniques in practice. More detailed information can be found in the Course Description.
The information on this webpage is updated throughout the course, so check back regularly!
News
 Apr 8, 2014: The exam of Apr 10, 2014 will be in CTIZ 4.98.
 Feb 27, 2014: here are the solutions to the exam.
 Feb 19, 2014: Small corrections to results; these have been submitted.
 Feb 11, 2014: Results are now available.
 Jan 27, 2014: I solved the wrong exercise in part 3 of 5.4.1 (I gave the solution to \(\rho_{\{a \rightarrow b\}}(\partial_{\{a\}}(a + b + ab))\) instead of \(\rho_{\{a \rightarrow b\}}(\partial_{\{a,b\}}(a + b + ab))\)). This has how been corrected in the solutions.
 Jan 22, 2014: another fix to the solutions, 2.4.8.
 Jan 18, 2014: fixed solution to exercise 3.1.6.
 Jan 14, 2014: this is the appendix that will be provided at the exam.
 Jan 14, 2014: the hints in this document can be useful in improving the final version of your report.
Lectures
 Lecturer: dr.ir. Jeroen Keiren, HB 09.300 (only on Wednesdays, for the rest of the week at VU University Amsterdam, T453)
 Time and Location: Wednesdays, 08:4510:45, EWILecture hall M (note the changed location!)
Practical Project
 The assignment consists of designing a controller for a small embedded system. The standard project comprises the design and verification of a bridge. A more detailed description can be found in the Project Description. Alternatively, 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 up to four students.
Groups of up to 4 students are to be formed before November 18, 2013, 17.00h and the group composition is to be mailed to the lecturer. If you cannot find a group, let me know and I will place you in a group. For working on the practical project, on Wednesdays, 10:4515:45, EWILecture hall H is available.
 There are weekly group meetings with the lecturer on Wednesdays.
Time and Location: Wednesdays, 10:4515:45, v.d. Poelzaal (starting 20 November; location for 20 November to be announced).  Example reports of earlier years can be found here and here (posted with permission of the authors).
 The results of the practical assignment are only valid for a year, which means that, if you fail the course this year, you will have to redo the assignment next year.
For the practical project you need the mCRL2 toolset.
Material
 J.F. Groote and M.R. Mousavi. Modelling and Analysis of Communicating Systems, 2013 (Chapters 15), mandatory. The chapters are available through OpenCourseWare. Solutions to selected exercises
 J.J.A. Keiren. The modal µcalculus, 2013, mandatory. Available here. Solutions to mucalculus exercises
 L. Aceto, A. Ingólfsdóttir, K.G. Larsen and J. Srba. Reactive Systems. Cambridge. 2007. (recommended, in particular chapters 36).
 W.J. Fokkink. Modelling Distributed Systems: Protocol Verification with µCRL. Springer. 2011. (recommended) Check the author’s homepage for a PDF.
Some of the background material touched upon during the lectures:

K. Sandler, L. Ohrstrom, L. Moy and R. McVay: Killed by Code: Software Transparency in Implantable Medical Devices. Software Freedom Law Center. 2010. (Mentioned during lecture 1).
 J.F. Groote, T.W.D.M. Kouters and A.A.H. Osaiweran. Specification guidelines to avoid the state space explosion problem. Fundamentals of Software Engineering 2011, Proceedings. Lecture Notes in Computer Science 7141, Springer Verlag, pp. 112127, 2012. A more complete version appeared as technical report CSR 10/14. (Offers some modelling advice, and gives some examples of mCRL2 models).
 Some models of the coffee machine example discussed during the lecture can be found here.
Errata
 There is problem in the strong bisimulation example in the lecture notes, Figure 2.8. The relation \(R\) shown in the picture is not a strong bisimulation relation, since the \(b\) transition from \(t_2\) to \(t_4\) cannot be mimicked by \(s_2\) (the only possible \(b\) transition from \(s_2\) to \(s_4\) ends up in a state which is not related to \(t_4\)). This can be repaired by extending relation \(R\) such that also \(s_4 \mathrel{R} t_4\) and \(s_5 \mathrel{R} t_3\).
Schedule
Date  Topics  Slides  Exercises 

13 November 2013  Introduction to Behavioral Specification Behavioural Equivalences 
Intro Strong equivalences 
2.2.3, 2.3.2, 2.3.82.3.10 
20 November 2013  Behavioural Equivalences  Weak equivalences  2.3.82.3.10,2.4.62.4.8 
27 November 2013  Modal muCalculus  µcalculus  handout 2.42.5, 2.8, 2.112.12, 3.3, 4.2, 4.6, 4.8 
4 December 2013  Abstract Data Types  Abstract data types  3.1.23.1.8, 3.4.1, 3.5.13.5.3, 3.6.13.6.2 
11 December 2013  Sequential Processes: Theory  Sequential processes  4.2.3, 4.3.14.3.2, 4.4.1, 4.5.14.5.2, 4.6.1, 4.7.14.7.2, 4.8.1 
18 December 2013  Sequential Processes: Reasoning and Examples  Examples  
8 January 2014  Parallel Processes: Theory and Examples  Parallel Processes Examples 
5.1.15.1.2, 5.2.1, 5.3.15.3.2, 5.4.1, 5.5.1 
15 January 2014  Model Exam & Solutions 
Exam
 The final exam will be Thursday January 30, 2014, 9.0012.00.
 The resit exam will be Thursday April 10, 2014, 9.0012.00. Location: CTIZ 4.98
The types of questions that can be expected during the exam are detailed in the Assessment Guide. At the exam you will be provided with the following appendix.
Past Exams
The course was previously taught by Mohammad Mousavi. Here are a few of the exams of these years.
 Final exam of November 2, 2012. (Solutions)
 Resit exam of February 1, 2012. (Solutions)
 Final exam of November 10, 2011. (Solutions)
Older versions of this course
The course website for the 20122013 instalment of the course can be found here.