Catálogo de publicaciones - libros

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, 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 algorithms were wrong, this shows the decisive advantage of using an automatic prover in this context.

We present on an example the framework currently under development in the platform for proving that a or a C program is a correct implementation of some model defined by algebraic specifications, in a modular setting.

In this paper we present the part of the Coccinelle library which deals with list permutations. Indeed permutations naturally arise when formally modeling rewriting in , for instance RPO with multiset status and equality modulo AC. Moreover the needed permutations are up to an equivalence relation, and may be used to inductively define the same relation (equivalence modulo RPO). This is why we introduce the notion of permutation w. r. t. an arbitrary relation. The advantages of our approach are a very simple inductive definition (with only 2 constructors), the adequacy with the mathematical definition, the ability to define a relation using recursively permutations up to this very relation, and a fine grained modularity (if enjoys a property, so does ).