Proving correctness of transformation functions in collaborative editing systems

Gérald Oster 1 Pascal Urso 2 Pascal Molli 2 Abdessamad Imine 3
1 GlobIS - Global Information Systems Group [ETH Zürich]
D-INFK - Department of Computer Science [ETH Zürich]
2 ECOO - Environment for cooperation
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
3 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 : Operational transformation (OT) is an approach which allows to build real-time groupware tools. This approach requires correct transformation functions regarding two conditions called TP1 and TP2. Proving correctness of these transformation functions is very complex and error prone. In this paper, we show how a theorem prover can address this serious bottleneck. To validate our approach, we verifed correctness of state-of-art transformation functions de ned on strings of characters with surprising results. Counter-examples provided by the theorem prover helped us to design the tombstone transformation functions. These functions verify TP1 and TP2, preserve intentions and ensure multi-effect relationships.
Complete list of metadatas

Cited literature [28 references]  Display  Hide  Download

https://hal.inria.fr/inria-00071213
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 2:38:27 PM
Last modification on : Tuesday, March 5, 2019 - 9:30:10 AM
Long-term archiving on : Tuesday, February 22, 2011 - 11:51:04 AM

Identifiers

  • HAL Id : inria-00071213, version 1

Citation

Gérald Oster, Pascal Urso, Pascal Molli, Abdessamad Imine. Proving correctness of transformation functions in collaborative editing systems. [Research Report] RR-5795, INRIA. 2005, pp.45. ⟨inria-00071213⟩

Share

Metrics

Record views

678

Files downloads

445