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.
Type de document :
Communication dans un congrès
Sumitra Reddy and Mohammed Jmaiel. WETICE 2013: 22th IEEE International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises., Jun 2013, Hammamet, Tunisia. IEEE, 2013, 22nd IEEE WETICE Conference. 〈10.1109/WETICE.2013.44〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00862056
Contributeur : Dominique Méry <>
Soumis le : dimanche 15 septembre 2013 - 21:28:45
Dernière modification le : jeudi 11 janvier 2018 - 06:25:25

Identifiants

Citation

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

Partager

Métriques

Consultations de la notice

380