Symbolic Model-Checking of Optimistic Replication Algorithms

Hanifa Boucheneb 1 Abdessamad Imine 2, * Manal Najem 1
* Auteur correspondant
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.
Type de document :
Communication dans un congrès
Mery, Dominique and Merz, Stephan. 8th International Conference on Integrated Formal Methods - IFM 2010, Oct 2010, Nancy, France. Springer Berlin / Heidelberg, 6396, pp.89-104, 2010, Lecture Notes in Computer Science
Liste complète des métadonnées

Littérature citée [16 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00524535
Contributeur : Ist Inria Nancy Grand Est <>
Soumis le : vendredi 8 octobre 2010 - 10:04:59
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10
Document(s) archivé(s) le : jeudi 25 octobre 2012 - 16:40:50

Fichier

IFMSymbolicOT_89.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00524535, version 1

Citation

Hanifa Boucheneb, Abdessamad Imine, Manal Najem. Symbolic Model-Checking of Optimistic Replication Algorithms. Mery, Dominique and Merz, Stephan. 8th International Conference on Integrated Formal Methods - IFM 2010, Oct 2010, Nancy, France. Springer Berlin / Heidelberg, 6396, pp.89-104, 2010, Lecture Notes in Computer Science. 〈inria-00524535〉

Partager

Métriques

Consultations de la notice

355

Téléchargements de fichiers

139