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 -
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
- 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.
Next chapter: Modelling a system