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.

• Type: Journal
• Year: 2010
• Where: IFM
• Authors: Hanifa Boucheneb, Abdessamad Imine, Manal Najem
• Keywords: Convergence, Difference Bound Matrices, Formal Methods, IFM 2010, Operational Transformation