Learn to use formal techniques for specification and validation of communication protocols.
This course is concerned with specification and validation of protocols, using formal methods. The course is based on a specification language based on process algebra combined with abstract data types, called mCRL. This language and its toolset can be used for specification of parallel, communicating processes with data. Model checking is a method for expressing properties of concurrent finite-state systems, which can be checked automatically. Interesting properties of a specification are: "something bad will never happen" (safety), and "something good will eventually happen" (liveness). In the lab we will teach the use of a tool for automated verification of the required properties of a specification.
An overview of the subjects discussed in the respective lectures
An overview of the subjects discussed in the respective labs
There is a homework assignment available at the Labs web page, on a patient support system. This homework exercise will be marked, and this mark is taken into acount in the overall mark for the course (see below). The assignment can be carried out in groups of two or three persons.
For the exam you need to study the lecture notes, except chapter 5, the logics CTL and LTL in section 7.3, and sections 8.5-8.6.The overall mark of the course is (H+2W)/3, where H is the mark for the homework assignment, and W is the mark for the written exam.
During the exam you are allowed to use copies of the slides and of the lecture notes (without written comments!), except for the answers to the exercises as given at the end of the lecture notes.