System Validation (IN4387) 2013-2014

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 CT-IZ 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 + a|b))\) instead of \(\rho_{\{a \rightarrow b\}}(\partial_{\{a,b\}}(a + b + a|b))\)). 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, T-453)
  • Time and Location: Wednesdays, 08:45-10:45, EWI-Lecture 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:45-15:45, EWI-Lecture hall H is available.
  • There are weekly group meetings with the lecturer on Wednesdays.
    Time and Location: Wednesdays, 10:45-15: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 1-5), mandatory. The chapters are available through OpenCourseWareSolutions to selected exercises
  • J.J.A. Keiren. The modal µ-calculus, 2013, mandatory. Available hereSolutions to mu-calculus exercises
  • L. Aceto, A. Ingólfsdóttir, K.G. Larsen and J. Srba. Reactive Systems. Cambridge. 2007. (recommended, in particular chapters 3-6).
  • 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:

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.8-2.3.10
20 November 2013 Behavioural Equivalences Weak equivalences 2.3.8-2.3.10,2.4.6-2.4.8
27 November 2013 Modal mu-Calculus µ-calculus handout 2.4-2.5, 2.8, 2.11-2.12,
3.3, 4.2, 4.6, 4.8
4 December 2013 Abstract Data Types Abstract data types 3.1.2-3.1.8, 3.4.1,
3.5.1-3.5.3, 3.6.1-3.6.2
11 December 2013 Sequential Processes: Theory Sequential processes 4.2.3, 4.3.1-4.3.2,
4.4.1, 4.5.1-4.5.2, 4.6.1,
4.7.1-4.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.1-5.1.2, 5.2.1,
5.3.1-5.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.00-12.00.
  • The resit exam will be Thursday April 10, 2014, 9.00-12.00. Location: CT-IZ 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.

Older versions of this course

The course website for the 2012-2013 instalment of the course can be found here.