Deductive Verification of Distributed Groupware Systems

Abdessamad Imine 1 Pascal Molli 2 Gérald Oster 2 Michaël Rusinowitch 1
1 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
2 ECOO - Environment for cooperation
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Replication-based distributed systems consist of a group of users manipulating a shared object (like a text document, a filesystem, ...). Operational Transformation (OT) algorithms are applied for achieving convergence in these systems. However, the design of such algorithms is a difficult and error-prone activity, since building the correct operations for maintaining good convergence properties of the local copies requires examining a large number of situations. In this paper, we present the modelling and deductive verification of OT algorithms with algebraic specifications. We show that many OT algorithms in the litterature do no satisfy convergence properties unlike stated by their authors.
Type de document :
Communication dans un congrès
Charles Rattray and Savitri Maharaj and Carron Shankland. Tenth International Conference on Algebraic Methodology and Software Technology - AMAST 2004, 2004, Stirling, Scotland, United Kingdom, Springer, 3116, pp.226-240, 2004, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00099986
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 10:13:05
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10

Identifiants

  • HAL Id : inria-00099986, version 1

Citation

Abdessamad Imine, Pascal Molli, Gérald Oster, Michaël Rusinowitch. Deductive Verification of Distributed Groupware Systems. Charles Rattray and Savitri Maharaj and Carron Shankland. Tenth International Conference on Algebraic Methodology and Software Technology - AMAST 2004, 2004, Stirling, Scotland, United Kingdom, Springer, 3116, pp.226-240, 2004, Lecture Notes in Computer Science. 〈inria-00099986〉

Partager

Métriques

Consultations de la notice

195