nach oben

Erschienen in:

2016 | OriginalPaper | Buchkapitel

Verified Operational Transformation for Trees

verfasst von : Sergey Sinchuk, Pavel Chuprikov, Konstantin Solomatov

Erschienen in: Interactive Theorem Proving

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Operational transformation (OT) is an approach to concurrency control in groupware editors first proposed by C. Ellis and S. Gibbs in 1989. Google Wave and Google Docs are examples of better known OT-based systems and there are many other experimental ones described in the literature. In their recent articles A. Imine et al. have shown that many OT implementations contain mistakes and do not possess claimed consistency properties.

The present work describes an experimental library which is based on SSReflect/Coq and contains several operational transformation algorithms and proofs of their correctness.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Formalization of the Resolution Calculus for First-Order Logic

Nächstes Kapitel Hereditarily Finite Sets in Constructive Type Theory

Jetpad is a closed-source proprietary collaborative platform of JetBrains upon which several products such as CoachingSpaces or CensusAnalyzer are based.

https://github.com/JetBrains/ot-coq/blob/master/Comp.v.

https://github.com/JetBrains/ot-coq/blob/master/TreeOt.v.

https://github.com/JetBrains/ot-coq/blob/master/Fs.v.

https://github.com/JetBrains/ot-coq/blob/master/RichText.v.

https://github.com/JetBrains/ot-coq/blob/master/ListTools.v

Chlipala, A.: Certified Programming with Dependent Types. The MIT press, Cambridge (2013)MATH

Cormack, G.: A counterexample to the distributed operational transform and a corrected algorithm for point-to-point communication. Technical report, CS-95-06, Univ. Waterloo (1995). http://cs.uwaterloo.ca/research/tr/1995/08/dopt.pdf

Davis, A.H., Sun, C., Lu, J.: Generalizing operational transformation to the standard general markup language. In: Proceedings of Computer Supported Cooperative Work, pp. 58–67 (2002). http://dx.doi.org/10.1145/587078.587088

Ellis, C., Gibbs, S.: Concurrency control in groupware systems. In: Proceedings of 1989 ACM SIGMOD International Conference on Management of Data, vol. 18, pp. 399–407 (1989). http://dx.doi.org/10.1145/66926.66963

Gonthier, G., Mahboubi, A., Tassi, E.: A Small Scale Reflection Extension for the Coq system. Research Report RR-6455, Inria Saclay Ile de France (2015). https://hal.inria.fr/inria-00258384

Ignat, C.L., Norrie, M.C.: Customizable collaborative editor relying on treeOPT algorithm. In: Proceedings of 8th European Conference Computer Supported Cooperative Work, ECSCW 2003, pp. 315–334 (2003). http://citeseer.ist.psu.edu/viewdoc/download?doi=10.1.1.70.9273&rep=rep1&type=pdf

Imine, A., Rusinowitch, M., Molli, P., Oster, G.: Formal design and verification of operational transformation for copies convergence. Theor. Comput. Sci. 351(2), 167–183 (2006). http://dx.doi.org/10.1016/j.tcs.2005.09.066 MathSciNetCrossRefMATH

Lushman, B., Cormack, G.V.: Proof of correctness of Ressel’s adOPTed algorithm. Inform. Process. Lett. 86(6), 303–310 (2003). http://www.sciencedirect.com/science/article/pii/S0020019003002278 MathSciNetCrossRefMATH

Lushman, B., Roegist, A.: An automated verication of property tp2 for concurrent collaborative text buffers. Technical report, CS-2012-25, Univ. Waterloo, December 2012. http://cs.uwaterloo.ca/sites/ca.computer-science/files/uploads/files/CS-2012-25.pdf

10.

Randolph, A., Boucheneb, H., Imine, A., Quintero, A.: On consistency of operational transformation approach. Elec. Proc. Theor. Comput. Sci. 107, 45–59 (2013). http://dx.doi.org/10.4204/EPTCS.107.5 CrossRef

11.

Suleiman, M., Cart, M., Ferrié, J.: Concurrent operations in a distributed and mobile collaborative environment. In: Proceedings of 14th International Conference Data Engineering, Orlando, FL, USA, 23–27 February, pp. 36–45 (1998). http://dx.doi.org/10.1109/ICDE.1998.655755

12.

Sun, C.: Operational transformation frequently asked questions and answers (2010). http://cooffice.ntu.edu.sg/otfaq/

13.

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). http://dx.doi.org/10.1145/274444.274447 CrossRef

Titel: Verified Operational Transformation for Trees
verfasst von: Sergey Sinchuk
Pavel Chuprikov
Konstantin Solomatov
Verlag: Springer International Publishing
Buch: Interactive Theorem Proving
Print ISBN: 978-3-319-43143-7

Electronic ISBN: 978-3-319-43144-4

Copyright-Jahr: 2016
DOI: https://doi.org/10.1007/978-3-319-43144-4_22

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner