From Event-B Specifications to Programs for Distributed Algorithms

Abstract : 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.
Liste complète des métadonnées

https://hal.inria.fr/hal-00862056
Contributor : Dominique Méry <>
Submitted on : Sunday, September 15, 2013 - 9:28:45 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:03 PM

Identifiers

Citation

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⟩

Share

Metrics

Record views

435