Learning 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 µCRL. 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, using also the tool CADP. You need to ask for a (free) license for the latter tool. Interesting properties of a specification are: "something bad will never happen" (safety), or "something good will eventually happen" (liveness).
The lectures are based on Wan Fokkink, Modelling Distributed Systems: Protocol Verification with µCRL (2nd edition)
An overview of the subjects discussed in the respective lectures
An overview of the subjects discussed in the respective exercise classes
A homework assignment on a patient support system for MRI scanners is available here. 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 teams of up to 2 persons.
NEW! The deadline for handing it in has been extended to Monday June 13, at 10am. Students that meet the original deadline at May 23 will get a bonus point.
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 (without written comments!)