Component-Based Specification of Collaborative Objects

A collaborative object represents a data type (such as a text document or a spreadsheet) designed to be shared by multiple geographically separated users. In order to improve performance and availability of data in such a distributed context, each user has a local copy of the shared objects, upon which he may perform updates. Locally executed updates are then transmitted to the other users. So, the updates are applied in different orders at different copies of the collaborative object. This replication potentially leads, however, to divergent (i.e. different) copies. The Operational Transformation (OT) approach provides an interesting solution for copies divergence. Indeed, every collaborative object has an algorithm which transforms the remote update according to local concurrent ones. But this OT algorithm needs to fulfill two conditions in order to ensure the convergence. Proving the correctness of OT algorithms is very complex and error prone without the assistance of a theorem prover. In the present work, we propose a compositional method for specifying complex collaborative objects. The most important feature of our method is that designing an OT algorithm for the composed collaborative object can be done by reusing the OT algorithms of component collaborative objects. By using our method, we can start from correct small collaborative objects which are relatively easy to handle and incrementally combine them to build more complex collaborative objects