zbMATH — the first resource for mathematics

Formal design and verification of operational transformation algorithms for copies convergence. (English) Zbl 1086.68019
Summary: Distributed groupware systems provide computer support for manipulating objects such as a text document or a filesystem, shared by two or more geographically separated users. Data replication is a technology to improve performance and availability of data in distributed groupware systems. Indeed, 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. This replication potentially leads, however, to divergent (i.e. different) copies. In this respect, Operational Transformation (OT) algorithms are applied for achieving convergence of all copies, i.e. all users view the same objects. Using these algorithms users can exchange their updates in any order since the convergence should be ensured in all cases. However, the design of such algorithms is a difficult and error-prone activity since building the correct updates for maintaining good convergence properties of the local copies requires examining a large number of situations. In this paper, we present the modelling and deductive verification of OT algorithms with algebraic specifications. We show in particular that many OT algorithms in the literature do not satisfy convergence properties unlike what was stated by their authors.

68M14 Distributed systems
68Q65 Abstract data types; algebraic specification
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI
[1] Armando, A.; Rusinowitch, M.; Stratulat, S., Incorporating decision procedures in implicit induction, J. symbolic comput., 34, 4, 241-258, (2001) · Zbl 1037.68129
[2] Bidoit, M.; Hennicker, R.; Wirsing, M., Behavioural and abstractor specifications, Sci. comput. programming, 25, 2-3, 149-186, (1995) · Zbl 0853.68130
[3] Bouhoula, A.; Kounalis, E.; Rusinowitch, M., Automated mathematical induction, J. logic comput., 5, 5, 631-668, (1995) · Zbl 0832.68095
[4] Bouhoula, A.; Rusinowitch, M., Observational proofs by rewriting, Theoret. comput. sci., 275, 1-2, 675-698, (2002) · Zbl 1051.68085
[5] C.A. Ellis, S.J. Gibbs, Concurrency control in groupware systems, SIGMOD Conference 18, 1989.
[6] Ellis, C.A.; Gibbs, S.J.; Rein, G., Groupware: some issues and experiences, Commun. ACM, 34, 1, 39-58, (1991), (ISSN 0001-0782)
[7] J. Goguen, K. Lin, G. Roşu, Circular Coinductive Rewriting, Proc. 15th Internat. Conf. on Automated Software Engineering (ASE’00), Institute of Electrical and Electronics Engineers Computer Society, 2000, Grenoble, France, 11-15 September 2000.
[8] Goguen, J.; Malcolm, G., A hidden agenda, Theoret. comput. sci., 245, 1, 55-101, (2000) · Zbl 0946.68070
[9] A. Imine, P. Molli, G. Oster, M. Rusinowitch, Development of transformation functions assisted by a theorem prover, Fourth Internat. Workshop on Collaborative Editing (ACM CSCW’02), Collaborative Computing in IEEE Distributed Systems Online, November 2002. · Zbl 1086.68019
[10] A. Imine, P. Molli, G. Oster, M. Rusinowitch, Proving correctness of transformation functions in real-time groupware, in: Eighth European Conf. on Computer-supported Cooperative Work, Helsinki, Finland, 14-18 September 2003.
[11] Imine, A.; Molli, P.; Oster, G.; Urso, P., VOTE: group editors analyzing tool, ()
[12] Imine, A.; Urso, P., Automatic detection of copies divergence in collaborative editing systems, ()
[13] Lushman, B.; Cormack, G.V., Proof of correctness of Ressel’s adopted algorithm, Inform. process. lett., 86, 3, 303-310, (2003) · Zbl 1162.68373
[14] Molli, P.; Oster, G.; Skaf-Molli, H.; Imine, A., Using the transformational approach to build a safe and generic data synchronizer, (), (ISBN 1-58113-693-5)
[15] P. Molli, H. Skaf-Molli, G. Oster, S. Jourdain, SAMS: synchronous, asynchronous, multi-synchronous environments, The Seventh Internat. Conf. on CSCW in Design, Rio de Janeiro, Brazil, September 2002.
[16] M. Ressel, D. Nitsche-Ruhland, R. Gunzenhauser, An integrating, transformation-oriented approach to concurrency control and undo in group Editors, Proc. ACM Conf. on Computer Supported Cooperative Work (CSCW’96), Boston, MA, USA, November 1996.
[17] H. Shen, C. Sun, Flexible merging for asynchronous collaborative systems, On the Move to Meaningful Internet Systems, 2002—DOA/CoopIS/ODBASE 2002 Confederated International Conferences DOA, CoopIS and ODBASE 2002, Springer, Berlin, 2002 (ISBN 3-540-00106-9).
[18] M. Suleiman, M. Cart, J. Ferrié, Concurrent operations in a distributed and mobile collaborative environment, Proc. 14th Internat. Conf. on Data Engineering, February 23-27, 1998, Orlando, Florida, USA, IEEE Computer Society, Silver Spring, MD, 1998 (ISBN 0-8186-8289-2).
[19] Sun, C.; Ellis, C., Operational transformation in real-time group editors: issues, algorithms, and achievements, (), (ISBN 1-58113-009-0)
[20] Sun, C.; Jia, X.; Zhang, Y.; Yang, Y.; Chen, D., Achieving convergence, causality-preservation and intention-preservation in real-time cooperative editing systems, ACM trans. computer-human interaction (TOCHI), 5, 1, 63-108, (1998), (ISSN 1073-0516)
[21] D. Sun, S. Xia, C. Sun, D. Chen, Operational transformation for collaborative word processing, in: Proc. ACM 2004 Conf. on Computer Supported Cooperative Work, November 6-10, Chicago, IL USA, pp. 437-446.
[22] Tanenbaum, A.S., Distributed operating systems, (2002), Prentice-Hall, Inc EnglewoodCliffs, NJ, (ISBN 0-13-219908-4) · Zbl 0856.68041
[23] Terese, Term rewriting systems, (2003), Cambridge University Press Cambridge
[24] N. Vidot, M. Cart, J. Ferrié, M. Suleiman, Copies convergence in a distributed real-time collaborative environment, Proc. ACM Conf. on Computer Supported Cooperative Work (CSCW’00), Philadelphia, Pennsylvania, USA, December 2000.
[25] M. Wirsing, Algebraic Specification, Handbook of Theoretical Computer Science (Vol. B): Formal Models and Semantics, 1990, pp. 675-788. · Zbl 0900.68309
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.