On Model-Checking Optimistic Replication Algorithms - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2009

On Model-Checking Optimistic Replication Algorithms

Résumé

Collaborative editors consist of a group of users editing a shared document. The Operational Transformation (OT) approach is used for supporting optimistic replication in these editors. It allows the users to concurrently update the shared data and exchange their updates in any order since the convergence of all replicas, i.e. the fact that all users view the same data, is ensured in all cases. However, designing algorithms for achieving convergence with the OT approach is a critical and challenging issue. In this paper, we address the verification of OT algorithms with a model-checking technique. We formally define, using tool UPPAAL, the behavior and the convergence requirement of the collaborative editors, as well as the abstract behavior of the environment where these systems are supposed to operate. So, we show how to exploit some features of such systems and the tool UPPAAL to attenuate the severe state explosion problem. We have been able to show that if the number of users exceeds 2 then the convergence property is not satisfied for five OT algorithms. A counterexample is provided for every algorithm.

Dates et versions

inria-00431335 , version 1 (12-11-2009)

Identifiants

Citer

Hanifa Boucheneb, Abdessamad Imine. On Model-Checking Optimistic Replication Algorithms. 11th IFIP WG 6.1 International Conference FMOODS 2009 and 29th IFIP WG 6.1 International Conference FORTE 2009, Jun 2009, Lisbonne, Portugal. pp.73-89, ⟨10.1007/978-3-642-02138-1_5⟩. ⟨inria-00431335⟩
139 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More