Symbolic Model-Checking of Optimistic Replication Algorithms

Hanifa Boucheneb (1) , Abdessamad Imine (2) , Manal Najem (1)

1 VeriForm - Laboratoire VeriForm - Department of Computer Engineering
2 CASSIS - Combination of approaches to the security of infinite states systems

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.

Mots clés: collaborative editors; operational transformation; difference bound matrices; symbolic model checking; convergence property

Domaines: Génie logiciel [cs.SE]; Logique en informatique [cs.LO]

Hanifa Boucheneb, Abdessamad Imine, Manal Najem. Symbolic Model-Checking of Optimistic Replication Algorithms. 8th International Conference on Integrated Formal Methods - IFM 2010, INRIA Nancy Grand Est, Oct 2010, Nancy, France. pp.89-104. ⟨inria-00524535⟩