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:

• A brief manual on debugging of µCRL specifications

• 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
  • On the alternating bit protocol. Use this file with data types and declarations of actions and communications as a starting point.
  
  
• 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
  • On the bounded retransmission protocol. Use this file as a starting point.
  
  
• 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