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 Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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 metadatas

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/inria-00524535
Contributor : Ist Inria Nancy Grand Est <>
Submitted on : Friday, October 8, 2010 - 10:04:59 AM
Last modification on : Friday, July 6, 2018 - 3:06:10 PM
Long-term archiving on : Thursday, October 25, 2012 - 4:40:50 PM

File

IFMSymbolicOT_89.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00524535, version 1

Citation

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⟩

Share

Metrics

Record views

522

Files downloads

255