From Event-B Specifications to Programs for Distributed Algorithms

Mohammed Tounsi (1) , Mohammed Mosbah (1, 2) , Dominique Méry (3, 4)

1 LaBRI - Laboratoire Bordelais de Recherche en Informatique
2 ENSEIRB - Ecole Nationale Supérieure d'Electronique, Informatique et Radiocommunications de Bordeaux
3 MOSEL - Proof-oriented development of computer-based systems
4 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems

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.

Mots clés: Distributed algorithms; Distributed systems; Event-B; Formal methods; Local computations Visidia

Domaines: Algorithme et structure de données [cs.DS]; Calcul parallèle, distribué et partagé [cs.DC]; Logique en informatique [cs.LO]

Mohammed Tounsi, Mohammed Mosbah, Dominique Méry. From Event-B Specifications to Programs for Distributed Algorithms. WETICE 2013: 22th IEEE International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises., Jun 2013, Hammamet, Tunisia. ⟨10.1109/WETICE.2013.44⟩. ⟨hal-00862056⟩