Sciweavers

ICDCSW
2000
IEEE

Games-Based Model Checking of Protocols: counting doesn't count

13 years 8 months ago
Games-Based Model Checking of Protocols: counting doesn't count
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 twophase commit example, we check some elementary properties.
Tim Kempster, Colin Stirling, Peter Thanisch
Added 31 Jul 2010
Updated 31 Jul 2010
Type Conference
Year 2000
Where ICDCSW
Authors Tim Kempster, Colin Stirling, Peter Thanisch
Comments (0)