Automatic Detection of Copies Divergence in Collaborative Editing Systems

International audienceThe design of collaborative editing (CE) system is a difficult and error-prone activity, since building the correct operations for maintaining good convergence properties of the local copies requires examining a large number of situations. The operational transformation is an approach which is used for achieving convergence in CE system. But, it imposes the verification of two conditions, C1 and C2, whose the proof is often difficult to handily produce and unmanageably complicated. In this paper, we present an initial version of a tool for automatically verifying these conditions. The input of our tool consists of a formal specification written in algorithmic style which gives the behaviour system and the functional description of the transformation algorithm. The tool builds an algebraic specification described in terms of conditional equations. As verification back-end we use an automated induction-based theorem prover. We show in this work how to support the development of transformation algorithms by an automatic theorem prover that allows for an automated analysis of the numerous cases and therefore allows to derive a formal proof of the convergence property of the resulting editor. We give two case studies about different group editors which confirm the viability of our tool