By means of a sample session this page gives a short introduction and overview of handling the Kit. It will be shown how one can specify a concurrent system in one of the modelling languages supported by the Kit (in this example Communicating Finite Automata - CFA) and verify system properties like deadlock-freeness, reachability, and liveness properties with the different verification techniques embedded in the Kit.

This sample session is structured into the following parts:

• Modelling a system as CFA
  This part introduces by means of an example how one can model a concurrent system in one of the supported modelling languages. First it will be shown how to specify the mutex algorithm of Dekker in the modelling language CFA.
• Checking a system for deadlock-freeness

One interesting task is checking a modelled system for deadlock-freeness. The Kit offers different algorithms for deadlock-checking, and we will show their use by means of an example.
• Checking reachability properties

The Kit supports several methods for checking reachability properties. In this part we show how the mutual exclusion for critical regions in the Dekker algorithm can be verified with these techniques.
• Checking safety and liveness properties

We express safety and liveness properties in terms of temporal logics like CTL and LTL. They are the most popular temporal logics, and together they can express all common safety and liveness properties. By means of an example we show how to define properties in terms of CTL and LTL and how one can apply the offered techniques for verifying these properties.