From Event-B Specifications to Programs for Distributed Algorithms

Formal proofs of distributed algorithms are long, hard and tedious. We propose a general approach, based on the formal method Event-B, to automatically generate correct programs of distributed algorithms. Our approach is implemented with a translation tool, called B2Visidia, that generates Java code from an Event-B specification related to distributed algorithms. The resulting code can be run on classical distributed computing systems. To execute the induced programs, we use a tool called Visidia that can be used for experimenting, testing and visualizing programs of distributed algorithms.