Skip to Main content Skip to Navigation
Conference papers

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 (UMR 6174), 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.
Complete list of metadatas
Contributor : Abdessamad Imine <>
Submitted on : Thursday, November 12, 2009 - 9:58:59 AM
Last modification on : Wednesday, September 16, 2020 - 10:43:02 AM

Links full text



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⟩



Record views