We show how model checking can be used for the verification of protocols underlying groupware systems. To this aim, we present a case study of those protocols underlying the Clock toolkit [GUN96,UG99] that are responsible for its concurrency control and distributed notification aspects. We abstract from the original specification of these protocols given in [Urn98] in order to obtain a less detailed specification (model) that nevertheless covers many issues of interest. We show that this model is very well amenable to model checking by addressing the formalisation and verification of a number of important issues for the correctness of groupware protocols in general, i.e. not limited to those underlying Clock. In particular, we address data consistency through distributed notification, view consistency, absence of (user) starvation, and key issues related to concurrency control. As a result, we contribute to the verification of Clock's underlying groupware protocols, which was attempted in [Urn98] with very limited success.
[GUN96] T.C.N. Graham, T. Urnes, and R. Nejabi, Efficient Distributed
Implementation of Semi-Replicated Synchronous Groupware, Proceedings
UIST'96, ACM Press, New York, NY, 1996, 1 - 10.
[UG99] T. Urnes and T.C.N. Graham, Flexibly Mapping Synchronous Groupware Architectures to Distributed Implementations, Proceedings DSVIS'99, Springer-Verlag, Wien, 1999, 133 - 148.
[Urn98] T. Urnes, Efficiently Implementing Synchronous Groupware, Ph.D. thesis, Department of Computer Science, York University, Toronto, 1998.