Abstract
The Operational Transformation (OT) approach, used in many collaborative editors, allows a group of users to concurrently update replicas of a shared object and exchange their updates in any order. The basic idea of this approach is to transform any received update operation before its execution on a replica of the object. This transformation aims to ensure the convergence of the different replicas of the object. However, designing transformation algorithms for achieving convergence is a critical and challenging issue. In this paper, we address the verification of OT algorithms with a symbolic model-checking technique. We show how to use the difference bound matrices to explore symbolically infinite state-spaces of such systems and provide symbolic counterexamples for the convergence property.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Behrmann, G., Bouyer, P., Larsen, K.G., Pelánek, R.: Lower and upper bounds in zone-based abstractions of timed automata. Theoretical Computer Science 8(3) (2006)
Bérard, B., Bouyer, P., Petit, A.: Analysing the pgm protocol with UPPAAL. International Journal of Production Research 42(14), 2773–2791 (2004)
Boucheneb, H., Imine, A.: On model-checking optimistic replication algorithms. In: FMOODS/FORTE, pp. 73–89 (2009)
Ellis, C.A., Gibbs, S.J.: Concurrency control in groupware systems. In: SIGMOD Conference, vol. 18, pp. 399–407 (1989)
Emerson, E.A.: Temporal and modal logic. In: Handbook of Theoretical Computer Science, ch. 16. Formal Methods and Semantics, vol. B (1990)
Imine, A., Molli, P., Oster, G., Rusinowitch, M.: Proving correctness of transformation functions in real-time groupware. In: ECSCW 2003, Helsinki, Finland (September 14-18, 2003)
Imine, A., Rusinowitch, M., Oster, G., Molli, P.: Formal design and verification of operational transformation algorithms for copies convergence. Theoretical Computer Science 351(2), 167–183 (2006)
Ressel, M., Nitsche-Ruhland, D., Gunzenhauser, R.: An integrating, transformation-oriented approach to concurrency control and undo in group editors. In: ACM CSCW 1996, Boston, USA, pp. 288–297 (November 1996)
Suleiman, M., Cart, M., Ferrié, J.: Serialization of concurrent operations in a distributed collaborative environment. In: ACM GROUP 1997, pp. 435–445 (November 1997)
Suleiman, M., Cart, M., Ferrié, J.: Concurrent operations in a distributed and mobile collaborative environment. In: IEEE ICDE 1998, pp. 36–45 (1998)
Sun, C., Ellis, C.: Operational transformation in real-time group editors: issues, algorithms and achievements. In: ACM CSCW 1998, pp. 59–68 (1998)
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. Comput.-Hum. Interact. 5(1), 63–108 (1998)
Sun, C., Xia, S., Sun, D., Chen, D., Shen, H., Cai, W.: Transparent adaptation of single-user applications for multi-user real-time collaboration. ACM Trans. Comput.-Hum. Interact. 13(4), 531–582 (2006)
Vidot, N., Cart, M., Ferrié, J., Suleiman, M.: Copies convergence in a distributed real-time collaborative environment. In: ACM CSCW 2000, Philadelphia, USA (December 2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boucheneb, H., Imine, A., Najem, M. (2010). Symbolic Model-Checking of Optimistic Replication Algorithms. In: Méry, D., Merz, S. (eds) Integrated Formal Methods. IFM 2010. Lecture Notes in Computer Science, vol 6396. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16265-7_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-16265-7_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16264-0
Online ISBN: 978-3-642-16265-7
eBook Packages: Computer ScienceComputer Science (R0)