Proving Correctness of Transformation Functions in Real-Time Groupware

Simple item page
dc.contributor.authorImine, Abdessamad
dc.contributor.authorMolli, Pascal
dc.contributor.authorOster, Gérald
dc.contributor.authorRusinowitch, Michaël
dc.date.accessioned2017-04-15T11:48:25Z
dc.date.available2017-04-15T11:48:25Z
dc.date.issued2003
dc.description.abstractOperational 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.
dc.identifier.doi10.1007/978-94-010-0068-0_15
dc.identifier.isbn978-94-010-0068-0
dc.language.isoen
dc.publisherKluwer Academic Publishers, Dordrecht, The Netherlands
dc.relation.ispartofECSCW 2003: Proceedings of the Eighth European Conference on Computer Supported Cooperative Work
dc.relation.ispartofseriesECSCW
dc.titleProving Correctness of Transformation Functions in Real-Time Groupware
dc.typeText
gi.citation.endPage293
gi.citation.startPage277
gi.citations.count46
gi.citations.elementLeon 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
gi.citations.elementJ. 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
gi.citations.elementG/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
gi.citations.elementWeihai 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
gi.citations.elementChengzheng 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
gi.citations.elementAhmed-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
gi.citations.elementChengzheng 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
gi.citations.elementAbdessamad 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
gi.citations.elementStephan 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
gi.citations.elementPaulo Sérgio Almeida (2024): Approaches to Conflict-free Replicated Data Types, In: ACM Computing Surveys 2(57), doi:10.1145/3695249
gi.citations.elementVictor 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
gi.citations.elementChengzheng 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
gi.citations.elementDu 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
gi.citations.elementDu 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
gi.citations.elementAbdessamad 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
gi.citations.elementThomas 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
gi.citations.elementWeihai 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
gi.citations.elementAbdessamad 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
gi.citations.elementD. 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
gi.citations.elementAbdessamad 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
gi.citations.elementHanifa 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
gi.citations.elementAbdessamad Imine (2009): Coordination Model for Real-Time Collaborative Editors, In: Lecture Notes in Computer Science, doi:10.1007/978-3-642-02053-7_12
gi.citations.elementHrvoje Matijević, Saša Vranić, Nikola Kranjčić, Vlado Cetl (2024): Real-Time Co-Editing of Geographic Features, In: ISPRS International Journal of Geo-Information 12(13), doi:10.3390/ijgi13120441
gi.citations.elementMehdi 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
gi.citations.elementAbdessamad 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
gi.citations.elementNuno 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
gi.citations.elementCristian 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
gi.citations.elementA. 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
gi.citations.elementWeihai 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
gi.citations.elementAurel 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
gi.citations.elementYang 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
gi.citations.elementMartin 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
gi.citations.elementMumtaz Ahmad, Abdessamad Imine (2015): Decentralized Collaborative Editing Platform, In: 2015 16th IEEE International Conference on Mobile Data Management, doi:10.1109/mdm.2015.26
gi.citations.elementMumtaz 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
gi.citations.elementAsma 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
gi.citations.elementAsma 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
gi.citations.elementDu 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
gi.citations.elementClaudia‐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
gi.citations.elementD. 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
gi.citations.elementMumtaz 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
gi.citations.elementAbdessamad 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
gi.citations.elementHanifa 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
gi.citations.elementAurel 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
gi.citations.elementJiangming 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
gi.conference.date14–18 September 2003
gi.conference.locationHelsinki, Finland
gi.conference.sessiontitleFull Papers

Files

Original bundle

1 - 1 of 1
Thumbnail Image
Name:
00187.pdf
Size:
582.55 KB
Format:
Adobe Portable Document Format
Download

License bundle

1 - 1 of 1
Thumbnail Image
Name:
license.txt
Size:
0 B
Format:
Item-specific license agreed upon to submission
Description:
Download

Collections

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