Model Checking Groupware Protocols

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 that are responsible for its concurrency control and distributed notification aspects. We abstract from the original specification of these protocols 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 elsewhere with very limited success.