Verification 2

Basic algorithms for equivalence and model checking, CCS and CWB.
Kripke Structures and CTL

Time:   April 4

Litterature:

In many cases CGP and JPK offers slightly different presentations of the same subjects. However, it is useful to have a look at both books.

• CTL
•  (**) JPK section 3.1, 3.2, 3.4, 3.6, 3.7, 3.8
• CCS
•  (*) Robin Milner: Communicating and Mobile Systems, relevant parts of PART I.
• Algorithms for Bisimulation
• (**) Estenfeld, Schneider, Taubner, Tiden: Computer Aided Verification of Parallel Processes. in A. Pfitzmann, E. Raubold (eds.): VIS'91 Verlässliche Informationssysteme Proceedings, Darmstadt 1991, Informatik Fachberichte Vol. 271, pp 208-226, Springer 1991.
• Modal mu-calculus
• (**) Estenfeld, Schneider, Taubner, Tiden: Computer Aided Verification of Parallel Processes.
• (**) Stirling: An introduction to modal and temporal logic for CCS.

• CWB (Concurrency Workbench)
• A short introduction to the Concurrency Workbench (English, and and Aalborg version)
• The Edinburgh Concurrency Workbench (Version 7.1) (On-line Users Manual).

Excercises:

JPK exercise 16, 18 in Chapter 4

Exercise 2 (to be handed in)

JPK exercises 23, 24 and 25.
Model the protocols in CCS and analyse the models using CWB instead of SMV.
Formulate the properties of mutual exclusion  and absence of starvation either as (weak) bisimulation equivalences or formulas of the modal mu-calculus.
Write a small report describing you models of the protocols and the analysis you made using CWB. Hand in your report to  Oliver Möller by April 25.