Sciweavers

IFM
2010
Springer

Symbolic Model-Checking of Optimistic Replication Algorithms

13 years 1 months ago
Symbolic Model-Checking of Optimistic Replication Algorithms
Abstract. The Operational Transformation (OT) approach, used in many collaborative editors, allows a group of users to concurrently update replicas of a shared object and exchange their updates in any order. The basic idea of this approach is to transform any received update operation before its execution on a replica of the object. This transformation aims to ensure the convergence of the different replicas of the object. However, designing transformation algorithms for achieving convergence is a critical and challenging issue. In this paper, we address the verification of OT algorithms with a symbolic model-checking technique. We show how to use the difference bound matrices to explore symbolically infinite state-spaces of such systems and provide symbolic counterexamples for the convergence property. Key words: collaborative editors; operational transformation; difference bound matrices; symbolic model checking; convergence property.
Hanifa Boucheneb, Abdessamad Imine, Manal Najem
Added 13 Feb 2011
Updated 13 Feb 2011
Type Journal
Year 2010
Where IFM
Authors Hanifa Boucheneb, Abdessamad Imine, Manal Najem
Comments (0)