Sciweavers

Share
BIRTHDAY
2007
Springer

Applying a Theorem Prover to the Verification of Optimistic Replication Algorithms

12 years 3 months ago
Applying a Theorem Prover to the Verification of Optimistic Replication Algorithms
Abstract. The Operational Transformation (OT) approach is a technique for supporting optimistic replication in collaborative and mobile systems. 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 this issue for the important case where the shared data has a linear structure such as lists, texts, ordered XML trees, etc. We analyze the problem and we propose a generic solution with its formal analysis. We also show in this work how to support the formal design of an OT algorithm with a rewrite-based theorem prover. This theorem prover enables us to envisage the large number of cases required for the correctness proof of the algorithm. Since the manual proofs of all previously published algori...
Abdessamad Imine, Michaël Rusinowitch
Added 12 Aug 2010
Updated 12 Aug 2010
Type Conference
Year 2007
Where BIRTHDAY
Authors Abdessamad Imine, Michaël Rusinowitch
Comments (0)
books