Skip to Main content Skip to Navigation
Reports

Generating Distributed Programs from Event-B Models

Horatiu Cirstea 1, 2 Alexis Grall 2, 1 Dominique Méry 1, 3, 2
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
2 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
Abstract : Distributed algorithms offer challenges in checking that they meet their specifications. Verification techniques can be extended to deal with the verification of safety properties of distributed algorithms. In this paper, we present an approach for combining correct-by-construction approaches and transformations of formal models (EVENT-B) into programs (DISTALGO) to address the design of verified distributed programs. We define a subset LB (Local EVENT-B) of the EVENT-B modelling language restricted to events modelling the classical actions of distributed programs as internal or local computations , sending messages and receiving messages. We define then transformations of the various elements of the LB language into DISTALGO programs. The general methodology consists in starting from a statement of the problem to program and then progressively producing an LB model obtained after several refinement steps of the initial LB model. The derivation of the LB model is not described in the current paper and has already been addressed in other works. The transformation of LB models into DISTALGO programs is illustrated through a simple example. The refinement process and the soundness of the transformation allow one to produce correct-by-construction distributed programs.
Complete list of metadatas

Cited literature [19 references]  Display  Hide  Download

https://hal.inria.fr/hal-02572971
Contributor : Dominique Méry <>
Submitted on : Thursday, May 14, 2020 - 12:04:43 AM
Last modification on : Friday, September 4, 2020 - 11:20:23 AM

File

technicalreport.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02572971, version 1

Collections

Citation

Horatiu Cirstea, Alexis Grall, Dominique Méry. Generating Distributed Programs from Event-B Models. [Research Report] LORIA UMR 7503 CNRS, INRIA, Université de LORRAINE. 2020, pp.36. ⟨hal-02572971⟩

Share

Metrics

Record views

83

Files downloads

219