Experiments in Model-Checking Optimistic Replication Algorithms

Hanifa Boucheneb 1 Abdessamad Imine 2, *
* 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 : This paper describes a series of model-checking experiments to verify optimistic replication algorithms based on Operational Transformation (OT) approach used for supporting collaborative edition. We formally define, using tool UPPAAL, the behavior and the main consistency requirement (i.e. convergence property) of the collaborative editing systems, as well as the abstract behavior of the environment where these systems are supposed to operate. Due to data replication and the unpredictable nature of user interactions, such systems have infinitely many states. So, we show how to exploit some features of the UPPAAL specification language to attenuate the severe state explosion problem. Two models are proposed. The first one, called concrete model, is very close to the system implementation but runs up against a severe explosion of states. The second model, called symbolic model, aims to overcome the limitation of the concrete model by delaying the effective selection and execution of editing operations until the construction of symbolic execution traces of all sites is completed. Experimental results have shown that the symbolic model allows a significant gain in both space and time. Using the symbolic model, we have been able to show that if the number of sites exceeds $2$ then the convergence property is not satisfied for all OT algorithms considered here. A counterexample is provided for every algorithm.
Complete list of metadatas

Cited literature [14 references]  Display  Hide  Download

https://hal.inria.fr/inria-00274423
Contributor : Rapport de Recherche Inria <>
Submitted on : Monday, April 21, 2008 - 10:50:42 AM
Last modification on : Friday, July 6, 2018 - 3:06:10 PM
Long-term archiving on : Tuesday, September 21, 2010 - 4:37:00 PM

Files

RR-6510.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00274423, version 2
  • ARXIV : 0804.3023

Citation

Hanifa Boucheneb, Abdessamad Imine. Experiments in Model-Checking Optimistic Replication Algorithms. [Research Report] RR-6510, INRIA. 2008, pp.49. ⟨inria-00274423v2⟩

Share

Metrics

Record views

493

Files downloads

197