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. Interesting properties of a specification are: "something bad will never happen" (safety), and "something good will eventually happen" (liveness). Labs will teach the use of the tools µCRL and CADP 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
NEW! The homework assignment can be made in a team of two persons. (It can also be made alone; this fact will however not be taken into account in the marking.) Deadline (hard as nails!): 19 December 2011, 10am.
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!)