Skip to Main content Skip to Navigation
New interface
Conference papers

Symbolic Model-Checking of Optimistic Replication Algorithms

Hanifa Boucheneb 1 Abdessamad Imine 2, * Manal Najem 1 
* Corresponding author
2 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 Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Complete list of metadata

Cited literature [16 references]  Display  Hide  Download
Contributor : Ist Inria Nancy Grand Est Connect in order to contact the contributor
Submitted on : Friday, October 8, 2010 - 10:04:59 AM
Last modification on : Friday, January 21, 2022 - 3:09:01 AM
Long-term archiving on: : Thursday, October 25, 2012 - 4:40:50 PM


Files produced by the author(s)


  • HAL Id : inria-00524535, version 1


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⟩



Record views


Files downloads