Title: From Event-B specifications to programs for distributed algorithms

Authors: Mohamed Tounsi; Mohamed Mosbah; Dominique Méry

Addresses: LaBRI, CNRS UMR 5800, University of Bordeaux 1, F-33400 Talence, France ' LaBRI, CNRS UMR 5800, University of Bordeaux 1, F-33400 Talence, France ' LORIA, CNRS UMR 7503, University of Lorraine, F-54506 Vandœuvre-lès-Nancy, France

Abstract: Formal proofs of distributed algorithms are long, hard and tedious. We propose a general approach, based on the Event-B formal method, 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 executed on classical distributed computing systems. To execute the resulting programs, we use a tool called Visidia that can be used for experimenting, testing and visualising programs of distributed algorithms.

Keywords: formal methods; Event-B; distributed algorithms; distributed computing; local computations modelling; graph relabelling system; Visidia platform; Rodin platform; Java code.

DOI: 10.1504/IJAACS.2016.079623

International Journal of Autonomous and Adaptive Communications Systems, 2016 Vol.9 No.3/4, pp.223 - 242

Published online: 01 Oct 2016 *

Full-text access for editors Access for subscribers Purchase this article Comment on this article