Sciweavers

Share
AMAST
2004
Springer

Deductive Verification of Distributed Groupware Systems

9 years 3 months ago
Deductive Verification of Distributed Groupware Systems
Distributed groupware systems consist of a group of users manipulating a shared object (like a text document, a filesystem, etc). Operational Transformation (OT) algorithms are applied for achieving convergence in these systems. However, the design of such algorithms is a difficult and error-prone activity, since building the correct operations for maintaining good convergence properties of the local copies requires examining a large number of situations. In this paper, we present the modelling and deductive verification of OT algorithms with algebraic specifications. We show that many OT algorithms in the literature do not satisfy convergence properties unlike what was stated by their authors.
Abdessamad Imine, Pascal Molli, Gérald Oste
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2004
Where AMAST
Authors Abdessamad Imine, Pascal Molli, Gérald Oster, Michaël Rusinowitch
Comments (0)
books