Assisting Groupware Development with Model Checking – Case Studies from Cooperative Work in the WWW

摘要

Efficient collaboration entails significant benefits for modern enterprises. Recent advances in Internettechnology allow physically dispersed groups to bypass the obstacles raised by geographical distances, so thedevelopment of Internet based groupware may extend collaboration to a global scale. As groupware applications growlarger and more diverse, however, it becomes difficult to anticipate their correctness. In this paper, we address thisdifficulty within the context of group awareness, which we regard both as a communication issue and a user-interface one.The main contribution of our research is the use of symbolic model checking for verifying group awareness incollaborative work across the WWW. This involves the specification of two related protocols with temporal logic and thedevelopment of a methodology for encoding temporal formulae into the language of a symbolic model checker, whicheliminates the need to draw state-transition diagrams. Taking then advantage of the model checker’s ability to producecounterexamples, we discover drawbacks in these protocols and propose thereon a number of improvements, which aim totransform the WWW into a reliable collaborative environment.