On Model-Checking Optimistic Replication Algorithms

Hanifa Boucheneb 1 Abdessamad Imine 2
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, INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : 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.
Type de document :
Communication dans un congrès
David Lee and Antónia Lopes and Arnd Poetzsch-Heffter. 11th IFIP WG 6.1 International Conference FMOODS 2009 and 29th IFIP WG 6.1 International Conference FORTE 2009, Jun 2009, Lisbonne, Portugal. Springer, 5522, pp.73-89, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-02138-1_5〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00431335
Contributeur : Abdessamad Imine <>
Soumis le : jeudi 12 novembre 2009 - 09:58:59
Dernière modification le : jeudi 11 janvier 2018 - 06:20:00

Identifiants

Citation

Hanifa Boucheneb, Abdessamad Imine. On Model-Checking Optimistic Replication Algorithms. David Lee and Antónia Lopes and Arnd Poetzsch-Heffter. 11th IFIP WG 6.1 International Conference FMOODS 2009 and 29th IFIP WG 6.1 International Conference FORTE 2009, Jun 2009, Lisbonne, Portugal. Springer, 5522, pp.73-89, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-02138-1_5〉. 〈inria-00431335〉

Partager

Métriques

Consultations de la notice

261