Games-Based Model Checking of Protocols: counting doesn't count
Tim Kempster, Colin Stirling and Peter Thanisch
University of Edinburgh, Scotland, UK
Abstract
We introduce a technique that can be used to model the
behaviour of protocols. In our model each process within a
protocol belongs to a particular class. A set of rules governs
the behaviour of a process within a process class. The rules
give rise to a transition system that models the behaviour
of the protocol. By exploiting the homogeneous behavior of
a process within a particular class it is possible to model
the behaviour of an unbounded number of processes in a
way that results in a finite (and in most cases small) transition
system. We demonstrate this technique by modeling the
popular two-phase commit protocol. CTL properties can
be model checked in the resulting transition system using
a games based model checking algorithm. This technique
has the advantage that the entire transition system need not
always be generated. Furthermore, it provides evidence to
verify or refute the property being checked. Using the two
phase commit example, we check some elementary proper ties.
Keywords:
model checking, games, unbounded number of processes,
protocols