We have proposed a new approach called LC2B to give users guidliness for modelling and proving distributed algorithms. This approach is implemented with a tool that takes in parameter an algorithm encoded in local computations model and generates automatically the appropriate Event-B specifications. The algorithm is defined by the user through a graphical representation of some rewitting rules. Each rule design a computation step of the algorithm. We propose a DTD (Document Type Definition) to define a commun structre for rewrting rules encoding a distributed algorithm.

The process of LC2B is described as follows : a source file is prepared from the graphical representation with respect to the DTD structre. Once this file is generated, we perform two transformations to generate respectively the corresponding Event-B contexts and machine. To do so, we propose some particular rules written in XSLT(eXtensible Stylesheet Language Transformations).

A Java implementation can be generated automatically from the resulting Event-B code using a translation tool called B2Visida. The resulting implementation can be subsequently executed on the Visidia environment for visualizing and experimenting distributed algorithms.