Protocol Validation - Labs and Exercise Classes
As the material of the course has both theoretical and practical aspects,
there are both exercise classes concerning the theoretical part taught
in a lecture room, and computer labs that take place in a computer room.
Overview of the exercise classes and labs:
The numbers of the exercises refer to the 2nd edition!
- Lecture 1 is accompanied by an exercise class
- abstract data types: exercises 1(<=>), 2(>,even), 4(head,toe,tail,untoe,++), 5, 6
- induction: exercises 8(7,9), 10;
- process algebra: exercises 12(3), 18, 20, 22
- Lecture 2 is accompanied by a computer lab
- On two buffers that are
put in sequence, together with a brief manual regarding the
installation and use of the µCRL toolset.
To use
the µCRL toolset, you need to set the following paths in .bashrc:
export PATH=/usr/local/mcrl-2.18.1/bin:$PATH
And in order to use CADP, you need to set:
export CADP=/usr/local/CADP-2010-c
export PATH=$CADP:$CADP/com:$CADP/bin.x64:$PATH
- Lecture 3 is accompanied by a computer lab
- Lecture 4 is accompanied by an exercise class
- hiding: exercises 40(4,5), 41
- linearisation: exercises 59, 60, 61
- state space generation: exercise 62
- describe global requirements of the patient support system presented in the homework assignment, as well as an architecture for the components of this system.
- Lecture 5 is accompanied by an exercise class
- minimisation modulo branching bisimulation: exercise 63(1,2,3,5,6,7)
- mu-calculus: exercises 67(1,2), 70, 71, 72
- Lecture 6 is accompanied by a computer lab
- Lecture 7 is accompanied by an exercise class
- regular mu-calculus: 75, 76
- invariants: exercise 84
- CL-RSP: exercise 86
- cones and foci: exercises 87, 88, 90
- Lecture 8 is not accompanied by an exercise class or computer lab
- Lecture 9 is accompanied by an exercise class
- confluence: exercises 65, 66
- partial order reduction: exercises 92, 93
- Lecture 10 is not accompanied by an exercise class or computer lab
- Lecture 11 is accompanied by an exercise class
- distributed state space generation: exercise 78
- abstraction: exercises 79, 80, 81
- old exam