PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Ter Beek M. H., Massink M., Latella D., Gnesi S. Model Checking Groupware Protocols. The document has been submitted to Conference: 6th International Conference on the Design of Cooperative Systems (COOP'04), Technical report, 2003.
 
 
Abstract
(English)
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.
Subject Groupware protocols
Model checking
Concurrency
Clock toolkit
D.2.4 Software/Program Verification: Formal methods, D.2.4


Icona documento 1) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional