Formal Design and Verification of Operational Transformation Algorithms for Copies Convergence

Abdessamad Imine 1 Michaël Rusinowitch 1 Gérald Oster 2 Pascal Molli 2
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
2 ECOO - Environment for cooperation
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Distributed groupware systems provide computer support for manipulating objects such as a text document or a filesystem, shared by two or more geographically separated users. Data replication is a technology to improve performance and availability of data in distributed groupware systems. Indeed, each user has a local copy of the shared objects, upon which he may perform updates. Locally executed updates are then transmitted to the other users. This replication potentially leads, however, to divergent (i.e. different) copies. In this respect, Operational Transformation (OT) algorithms are applied for achieving convergence of all copies, i.e. all users view the same objects. Using these algorithms users can exchange their updates in any order since the convergence should be ensured in all cases. However, the design of such algorithms is a difficult and error-prone activity since building the correct updates 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 in particular that many OT algorithms in the literature do not satisfy convergence properties unlike what was stated by their authors.
Document type :
Journal articles
Complete list of metadatas

https://hal.inria.fr/inria-00000426
Contributor : Pascal Molli <>
Submitted on : Wednesday, October 12, 2005 - 3:56:27 PM
Last modification on : Friday, April 12, 2019 - 10:18:03 AM

Links full text

Identifiers

Citation

Abdessamad Imine, Michaël Rusinowitch, Gérald Oster, Pascal Molli. Formal Design and Verification of Operational Transformation Algorithms for Copies Convergence. Theoretical Computer Science, Elsevier, 2006, Algebraic Methodology and Software Technology, 351 (2), pp.167--183. ⟨10.1016/j.tcs.2005.09.066⟩. ⟨inria-00000426⟩

Share

Metrics

Record views

347