Treffer: From Event-B Specifications to Programs for Distributed Algorithms
Title:
From Event-B Specifications to Programs for Distributed Algorithms
Authors:
Contributors:
Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Centre National de la Recherche Scientifique (CNRS), Ecole Nationale Supérieure d'Electronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), Proof-oriented development of computer-based systems (MOSEL), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Centre Inria de l'Université de Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-CentraleSupélec-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Sumitra Reddy and Mohammed Jmaiel, ANR-06-SETI-0015,RIMEL,Raffinement Incrémental de Modèles EvènementieLs(2006)
Source:
WETICE 2013: 22th IEEE International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises., Jun 2013, Hammamet, Tunisia. ⟨10.1109/WETICE.2013.44⟩
Publisher Information:
CCSD; IEEE, 2013.
Publication Year:
2013
Collection:
collection:CNRS
collection:INRIA
collection:ENSEIRB
collection:UNIV-BORDEAUX
collection:INRIA_TEST
collection:LORIA2
collection:INRIA-NANCY-GRAND-EST
collection:TESTALAIN1
collection:TESTBORDEAUX
collection:UNIV-LORRAINE
collection:INRIA2
collection:LORIA
collection:LORIA-FM
collection:ANR
collection:INRIA-ALLEMAGNE
collection:UNIVERSITE-BORDEAUX
collection:AM2I-UL
collection:FORM_BORDEAUX_7
collection:INRIA
collection:ENSEIRB
collection:UNIV-BORDEAUX
collection:INRIA_TEST
collection:LORIA2
collection:INRIA-NANCY-GRAND-EST
collection:TESTALAIN1
collection:TESTBORDEAUX
collection:UNIV-LORRAINE
collection:INRIA2
collection:LORIA
collection:LORIA-FM
collection:ANR
collection:INRIA-ALLEMAGNE
collection:UNIVERSITE-BORDEAUX
collection:AM2I-UL
collection:FORM_BORDEAUX_7
Subject Terms:
Distributed algorithms, Distributed systems, Event-B, Formal methods, Local computations Visidia, [INFO.INFO-DS]Computer Science [cs], Data Structures and Algorithms [cs.DS], [INFO.INFO-DC]Computer Science [cs], Distributed, Parallel, and Cluster Computing [cs.DC], [INFO.INFO-LO]Computer Science [cs], Logic in Computer Science [cs.LO]
Subject Geographic:
Original Identifier:
HAL: hal-00862056
Document Type:
Konferenz
conferenceObject<br />Conference papers
Language:
English
Relation:
info:eu-repo/semantics/altIdentifier/doi/10.1109/WETICE.2013.44
DOI:
10.1109/WETICE.2013.44
Availability:
Accession Number:
edshal.hal.00862056v1
Database:
HAL
Weitere Informationen
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.