Paper Info
Title
Formal Verification of Operational Transformation.
Abstract
Operational Transformation (OT) is a technology to provide consistency maintenance and concurrency control in real-time collaborative editing systems. The correctness of OT is critical due to its foundation role in supporting a wide range of real world applications. In this work, we formally model the OT-based collaborative editing systems and establish their correctness, w.r.t. convergence and intention preservation, using a set of well-defined transformation conditions and properties. We then use model checking to verify the transformation properties for basic data and operational models. To the best of our knowledge, this is the first work to conduct a complete verification of OT including control algorithms and transformation functions. Our evaluation confirmed the correctness of existing OT systems and transformation functions with important discoveries.
Year
DOI
Venue
2014
10.1007/978-3-319-06410-9_30
Lecture Notes in Computer Science
Field
DocType
Volume
Convergence (routing),Transformation (function),Model checking,Operational transformation,Concurrency control,Collaborative editing,Computer science,Correctness,Theoretical computer science,Formal verification
Conference
8442
ISSN
Citations 
PageRank 
0302-9743
2
0.37
References 
Authors
12
4
Name
Order
Citations
PageRank
Yang Liu12194188.81
Yi Xu21757177.61
Shao Jie Zhang3564.71
chengzheng sun41363101.83