Text Document

Proving Correctness of Transformation Functions in Real-Time Groupware

Thumbnail Image

Fulltext URI

Document type

Text

Files

00187.pdf (582.55 KB)

Additional Information

Date

2003

Authors

Journal Title

Journal ISSN

Volume Title

Source

ECSCW 2003: Proceedings of the Eighth European Conference on Computer Supported Cooperative Work
Full Papers

Publisher

Kluwer Academic Publishers, Dordrecht, The Netherlands

Abstract

Operational transformation is an approach which allows to build real-time groupware tools. This approach requires correct transformation functions. Proving the correction of these transformation functions is very complex and error prone. In this paper, we show how a theorem prover can address this serious bottleneck. To validate our approach, we have verified the correctness of state-of-art transformation functions defined on Strings with surprising results. Counter-examples provided by the theorem prover have helped us to define new correct transformation functions for Strings.

Description

Imine, Abdessamad; Molli, Pascal; Oster, Gérald; Rusinowitch, Michaël (2003): Proving Correctness of Transformation Functions in Real-Time Groupware. ECSCW 2003: Proceedings of the Eighth European Conference on Computer Supported Cooperative Work. DOI: 10.1007/978-94-010-0068-0_15. Kluwer Academic Publishers, Dordrecht, The Netherlands. ISBN: 978-94-010-0068-0. pp. 277-293. Full Papers. Helsinki, Finland. 14–18 September 2003

Keywords

Citation

DOI

10.1007/978-94-010-0068-0_15

URI

URI

Collections

ECSCW 2003: Proceedings of the Eighth European Conference on Computer Supported Cooperative Work

Endorsement

Review

Supplemented By

Referenced By

Number of citations to item: 45

  • G/l=e'/rald Oster, Pascal Molli, Pascal Urso, Abdessamad Imine (2006): Tombstone Transformation Functions for Ensuring Consistency in Collaborative Editing Systems, In: 2006 International Conference on Collaborative Computing: Networking, Applications and Worksharing, doi:10.1109/colcom.2006.361867
  • Nuno Preguiça, J. Legatheaux Martins, Henrique Domingos, Sérgio Duarte (2005): Integrating Synchronous and Asynchronous Interactions in Groupware Applications, In: Lecture Notes in Computer Science, doi:10.1007/11560296_7
  • Abdessamad Imine (2008): Flexible Concurrency Control for Real-Time Collaborative Editors, In: 2008 The 28th International Conference on Distributed Computing Systems Workshops, doi:10.1109/icdcs.workshops.2008.91
  • Abdessamad Imine, Pascal Urso (2003): Automatic Detection of Copies Divergence in Collaborative Editing Systems1 1The authors would like to thank Pascal Molli and Gérald Oster for useful comments on an earlier draft of this paper., In: Electronic Notes in Theoretical Computer Science, doi:10.1016/s1571-0661(04)80811-9
  • Weihai Yu, Luc André, Claudia-Lavinia Ignat (2015): A CRDT Supporting Selective Undo for Collaborative Text Editing, In: Lecture Notes in Computer Science, doi:10.1007/978-3-319-19129-4_16
  • Chengzheng Sun (2017): Reflections on collaborative editing research: From academic curiosity to real-world application, In: 2017 IEEE 21st International Conference on Computer Supported Cooperative Work in Design (CSCWD), doi:10.1109/cscwd.2017.8066663
  • D. Li, R. Li (2004): Ensuring content and intention consistency in real-time group editors, In: 24th International Conference on Distributed Computing Systems, 2004. Proceedings., doi:10.1109/icdcs.2004.1281643
  • Paulo Sérgio Almeida (2024): Approaches to Conflict-free Replicated Data Types, In: ACM Computing Surveys 2(57), doi:10.1145/3695249
  • Hanifa Boucheneb, Abdessamad Imine (2009): On Model-Checking Optimistic Replication Algorithms, In: Lecture Notes in Computer Science, doi:10.1007/978-3-642-02138-1_5
  • Cristian Gadea, Bogdan Ionescu, Dan Ionescu (2018): Modeling and Simulation of an Operational Transformation Algorithm Using Finite State Machines, In: 2018 IEEE 12th International Symposium on Applied Computational Intelligence and Informatics (SACI), doi:10.1109/saci.2018.8440930
  • Claudia‐Lavinia Ignat, Luc André, Gérald Oster (2017): Enhancing rich content wikis with real‐time collaboration, In: Concurrency and Computation: Practice and Experience 8(33), doi:10.1002/cpe.4110
  • Asma Cherif, Abdessamad Imine (2016): Using CSP for coordinating undo-based collaborative applications, In: Proceedings of the 31st Annual ACM Symposium on Applied Computing, doi:10.1145/2851613.2851753
  • Du Li, Rui Li (2006): An Operational Transformation Algorithm and Performance Evaluation, In: Computer Supported Cooperative Work (CSCW) 5-6(17), doi:10.1007/s10606-005-9008-6
  • Yang Liu, Yi Xu, Shao Jie Zhang, Chengzheng Sun (2014): Formal Verification of Operational Transformation, In: Lecture Notes in Computer Science, doi:10.1007/978-3-319-06410-9_30
  • D. Sun, Chengzheng Sun (2009): Context-Based Operational Transformation in Distributed Collaborative Editing Systems, In: IEEE Transactions on Parallel and Distributed Systems 10(20), doi:10.1109/tpds.2008.240
  • Martin Kleppmann, Alastair R. Beresford (2017): A Conflict-Free Replicated JSON Datatype, In: IEEE Transactions on Parallel and Distributed Systems 10(28), doi:10.1109/tpds.2017.2697382
  • A. Jesse Jiryu Davis, Max Hirschhorn, Judah Schvimer (2020): Extreme modelling in practice, In: Proceedings of the VLDB Endowment 9(13), doi:10.14778/3397230.3397233
  • Hanifa Boucheneb, Abdessamad Imine, Manal Najem (2010): Symbolic Model-Checking of Optimistic Replication Algorithms, In: Lecture Notes in Computer Science, doi:10.1007/978-3-642-16265-7_8
  • Chengzheng Sun, David Sun, Agustina Ng, Weiwei Cai, Bryden Cho (2020): Real Differences between OT and CRDT under a General Transformation Framework for Consistency Maintenance in Co-Editors, In: Proceedings of the ACM on Human-Computer Interaction GROUP(4), doi:10.1145/3375186
  • Leon Freudenthaler (2024): Decentralized Near-Synchronous Local-First Programming Collaboration, In: Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis, doi:10.1145/3650212.3685555
  • Abdessamad Imine, Michaël Rusinowitch, Gérald Oster, Pascal Molli (2006): Formal design and verification of operational transformation algorithms for copies convergence, In: Theoretical Computer Science 2(351), doi:10.1016/j.tcs.2005.09.066
  • Du Li, Rui Li (2009): An Admissibility-Based Operational Transformation Framework for Collaborative Editing Systems, In: Computer Supported Cooperative Work (CSCW) 1(19), doi:10.1007/s10606-009-9103-1
  • Mumtaz Ahmad, Abdessamad Imine (2015): Decentralized Collaborative Editing Platform, In: 2015 16th IEEE International Conference on Mobile Data Management, doi:10.1109/mdm.2015.26
  • Ahmed-Nacer Mehdi, Pascal Urso, François Charoy (2015): Merging By Decentralized Eventual Consistency Algorithms, In: EAI Endorsed Transactions on Collaborative Computing 6(1), doi:10.4108/eai.21-12-2015.150817
  • Chengzheng Sun, Yi Xu, Agustina Ng (2017): Exhaustive Search and Resolution of Puzzles in OT Systems Supporting String-Wise Operations, In: Proceedings of the 2017 ACM Conference on Computer Supported Cooperative Work and Social Computing, doi:10.1145/2998181.2998252
  • Abdessamad Imine, Michaël Rusinowitch (2000): Applying a Theorem Prover to the Verification of Optimistic Replication Algorithms, In: Lecture Notes in Computer Science, doi:10.1007/978-3-540-73147-4_11
  • Aurel Randolph, Hanifa Boucheneb, Abdessamad Imine, Alejandro Quintero (2015): On Synthesizing a Consistent Operational Transformation Approach, In: IEEE Transactions on Computers 4(64), doi:10.1109/tc.2014.2308203
  • Aurel Randolph, Hanifa Boucheneb, Abdessamad Imine, Alejandro Quintero (2013): On Consistency of Operational Transformation Approach, In: Electronic Proceedings in Theoretical Computer Science, doi:10.4204/eptcs.107.5
  • Jiangming Yang, Qiwei Zhang, Ning Gu, Genxing Yang, Zhenyu Liu (2005): The Multi-version and Single-display Strategy in Undo Scheme, In: The Fifth International Conference on Computer and Information Technology (CIT'05), doi:10.1109/cit.2005.189
  • Du Li, Rui Li (2006): An Approach to Ensuring Consistency in Peer-to-Peer Real-Time Group Editors, In: Computer Supported Cooperative Work (CSCW) 5-6(17), doi:10.1007/s10606-005-9009-5
  • Thomas B. Hodel-Widmer, Klaus R. Dittrich (2005): Concept and prototype of a collaborative business process environment for document processing, In: Data & Knowledge Engineering 1(52), doi:10.1016/j.datak.2004.06.004
  • J. Nathan Foster, Michael B. Greenwald, Christian Kirkegaard, Benjamin C. Pierce, Alan Schmitt (2007): Exploiting schemas in data synchronization, In: Journal of Computer and System Sciences 4(73), doi:10.1016/j.jcss.2006.10.024
  • Weihai Yu, Gérald Oster, Claudia-Lavinia Ignat (2017): Handling Disturbance and Awareness of Concurrent Updates in a Collaborative Editor, In: Lecture Notes in Computer Science, doi:10.1007/978-3-319-66805-5_5
  • Abdessamad Imine (2009): Coordination Model for Real-Time Collaborative Editors, In: Lecture Notes in Computer Science, doi:10.1007/978-3-642-02053-7_12
  • Mumtaz Ahmad, Abdessamad Imine, Mahfoud Houari (2015): A Highly Concurrent Replicated Data Structure EAI Endorsed Transactions, In: EAI Endorsed Transactions on Collaborative Computing 6(1), doi:10.4108/eai.21-12-2015.150820
  • Stephan A. Kollmann, Martin Kleppmann, Alastair R. Beresford (2019): Snapdoc: Authenticated snapshots with history privacy in peer-to-peer collaborative editing, In: Proceedings on Privacy Enhancing Technologies 3(2019), doi:10.2478/popets-2019-0044
  • Weihai Yu (2014): Supporting String-Wise Operations and Selective Undo for Peer-to-Peer Group Editing, In: Proceedings of the 18th International Conference on Supporting Group Work, doi:10.1145/2660398.2660401
  • Mumtaz Ahmad (2015): Collaborative distributed editing (Real number based indexation), In: 2015 International Symposium on Networks, Computers and Communications (ISNCC), doi:10.1109/isncc.2015.7238587
  • Asma Cherif, Abdessamad Imine (2015): A Constraint-based Approach for Generating Transformation Patterns, In: Electronic Proceedings in Theoretical Computer Science, doi:10.4204/eptcs.201.4
  • Mehdi Ahmed-Nacer, Claudia-Lavinia Ignat, Gérald Oster, Hyun-Gul Roh, Pascal Urso (2011): Evaluating CRDTs for real-time document editing, In: Proceedings of the 11th ACM symposium on Document engineering, doi:10.1145/2034691.2034717
  • Victor B. F. Gomes, Martin Kleppmann, Dominic P. Mulligan, Alastair R. Beresford (2017): Verifying strong eventual consistency in distributed systems, In: Proceedings of the ACM on Programming Languages OOPSLA(1), doi:10.1145/3133933
  • Abdessamad Imine, Pascal Molli, Gérald Oster, Michaël Rusinowitch (2005): Towards Synchronizing Linear Collaborative Objects with Operational Transformation, In: Lecture Notes in Computer Science, doi:10.1007/11562436_30
  • Abdessamad Imine, Pascal Molli, Gérald Oster, Michaël Rusinowitch (2004): Deductive Verification of Distributed Groupware Systems, In: Lecture Notes in Computer Science, doi:10.1007/978-3-540-27815-3_20
Please note: Providing information about citations is only possible thanks to to the open metadata APIs provided by crossref.org and opencitations.net. These lists may be incomplete due to unavailable citation data.source: opencitations.net, crossref.org