HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

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 Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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 metadata

Cited literature [28 references]  Display  Hide  Download

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Tuesday, May 23, 2006 - 2:38:27 PM
Last modification on : Friday, January 21, 2022 - 3:09:05 AM
Long-term archiving on: : Tuesday, February 22, 2011 - 11:51:04 AM


  • HAL Id : inria-00071213, version 1


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⟩



Record views


Files downloads