Proving Correctness of Transformation Functions in Real-Time Groupware
Published 1 January 2003
Abdessamad Imine, Pascal Molli, Gérald Oster, Michaël Rusinowitch
Citations100
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
This paper shows how a theorem prover can address this serious bottleneck of operational transformation, and verified the correctness of state-of-art transformation functions defined on Strings with surprising results.
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.
Keywords
Computer Science
ACM Transactions on Computer-Human InteractionAchieving convergence, causality preservation, and intention preservation in real-time cooperative editing systems
584 Citations1998Chengzheng Sun, Xiaohua Jia +3 more
A consistency model, with properties of convergence, causality preservation, and intention preservation, is proposed as a framework for consistency maintenance in real-time cooperative editing systems and an integrated set of schemes and algorithms are devised.
An integrating, transformation-oriented approach to concurrency control and undo in group editors
275 Citations1996Matthias Ressel, Doris Nitsche-Ruhland +1 more
An improved version of an existing distributed algorithm for concurrency control that is based on operation transformations is presented and a set of necessary and scientific conditions to be presented in order to ensure consistency in a replicated architecture is presented.
ACM Transactions on Computer-Human InteractionConsistency maintenance in real-time collaborative graphics editing systems
214 Citations2002Chengzheng Sun, David Chen
An object-level multiversioning approach to consistency maintenance in real-time collaborative graphic editors is proposed, which is novel in achieving intention preservation and convergence, in preserving the work concurrently produced by multiple users in the face of conflict, and in minimizing the number of object versions for conflict resolution.
Copies convergence in a distributed real-time collaborative environment
193 Citations2000Nicolas Vidot, Michelle Cart +2 more
Two new algorithms are presented that are based upon the impleðmentation of a continuous global order which enables that condition to be released, and simplifies the operation inteðgration process.
ACM Transactions on Computer-Human InteractionUndo as concurrent inverse in group editors
116 Citations2002Chengzheng Sun
The proposed undo solution consists of a generic transformation control algorithm that is capable of generating, transforming, and representing valid inverse operations in any context, and a set of transformation functions that are capable of preserving undo-related transformation conditions and properties.
Concurrent operations in a distributed and mobile collaborative environment
115 Citations2002Maher Suleiman, Michelle Cart +1 more
The principle objective of the paper is to present an algorithm that overcomes drawbacks in distributed and mobile collaborative environments based on the notion of user intention, and also on the construction of equivalent histories by exploiting and combining some general semantic properties such as forward/backward transposition.
Serialization of concurrent operations in a distributed collaborative environment
102 Citations1997Maher Suleiman, Michéle Cart +1 more
The principle objective of the this paper is to present an algorithm that overcomes problems of inconsistent copies, a non-respect of user’s intentions, and in the need to undo and redo certain operations.
Generalizing operational transformation to the standard general markup language
101 Citations2002Aguido Horatio Davis, Chengzheng Sun +1 more
This paper extends operational transformation to support synchronous collaborative editing of documents written in dialects of SGML such as XML and HTML, based on SGML's abstract data model, the grove, to make synchronous group editing applicable to the modern Web.
Journal of Automated ReasoningImplicit induction in conditional theories
93 Citations1995Adel Bouhoula, M. Rusinowitch
A new procedure for proof by induction in conditional theories where case analysis is simulated by term rewriting, which reduces considerably the number of variables of a conjecture to be considered for applying induction schemes.
Journal of Symbolic ComputationA General Framework to Build Contextual Cover Set Induction Provers
48 Citations2001Sorin Stratulat
This paper presents an abstract inference system uniformly defined in terms of contextual cover sets as a general framework to build implicit induction provers and shows that it generalizes existing cover set induction procedures.
SAMS: synchronous, asynchronous, multi-synchronous environments
48 Citations2003Pascal Molli, Hala Skaf‐Molli +2 more
A SAMS environment allows team members to work in synchronous, asynchronous or multi-synchronous mode while ensuring the coherence of shared data.
Operation transforms for a distributed shared spreadsheet
38 Citations1998Christopher R. Palmer, Gordon V. Cormack
The construction of operation transforms for a more sophisticated group of operations necessary for a shared spreadsheet, identifying a set of abstract operations thatacterize the operations on a spreadsheet.
HAL (Le Centre pour la Communication Scientifique Directe)Development of Transformation Functions Assisted by a Theorem Prover
13 Citations2002Abdessamad Imine, Pascal Molli +2 more