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...

• Type: Conference
• Year: 2007
• Where: BIRTHDAY
• Authors: Abdessamad Imine, Michaël Rusinowitch
• Keywords: Applied Computing, BIRTHDAY 2007, OT Approach, Rewrite-based Theorem Prover, Theorem Prover