Protocol Validation


Course Objective

Learning to use formal techniques for specification and validation of
communication protocols.

Course Content

This course is concerned with the 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 the
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.

Teaching Methods

4 hours per week HC
2 hours per week WC/PR (mixed)

During the practicum the mCRL2 toolset will be used for the validation
of protocols discussed during lectures. This toolset is freely available
for Windows, Linux, Mac (see

Method of Assessment

Written exam, together with a practical homework assignment. 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.


Wan Fokkink, Modelling Distributed Systems, Springer 2007. An online
version of this book (2nd edition) will be available.

Target Audience

mAI, mCS, mPDCS, master of Logic

Recommended background knowledge

Basic knowledge in mathematics and propositional logic, e.g. as dealt
with in the course "Logica en Modelleren"

General Information

Course Code X_400117
Credits 6 EC
Period P1
Course Level 500
Language of Tuition English
Faculty Faculty of Science
Course Coordinator dr. A. Ponse
Examiner dr. A. Ponse
Teaching Staff

Practical Information

You need to register for this course yourself

Last-minute registration is available for this course.

Teaching Methods Seminar, Lecture, Practical
Target audiences

This course is also available as: