Skip to Main content Skip to Navigation
Journal articles

From global choreographies to verifiable efficient distributed implementations

Abstract : We define a method to automatically synthesize efficient distributed implementations from high-level global choreographies. A global choreography describes the execution and communication logic between a set of provided processes which are described by their interfaces. At the choreography level, the operations include multiparty communications, choice, loop, and branching. A choreography is master triggered: it has one master to trigger its execution. This allows us to automatically generate conflict-free distributed implementations without controllers. The behavior of the synthesized implementations follows the behavior of choreographies. In addition, the absence of controllers ensures the efficiency of the implementation and reduces the communication needed at runtime. Moreover, we define a translation of the distributed implementations to equivalent Promela versions. The translation allows verifying the distributed system against behavioral properties. We implemented a Java prototype to validate the approach and applied it to automatically synthesize micro-service architectures. We also illustrate our method on the automatic synthesis of a verified distributed buying system.
Complete list of metadata

https://hal.inria.fr/hal-03113398
Contributor : Yliès Falcone Connect in order to contact the contributor
Submitted on : Monday, January 18, 2021 - 12:52:11 PM
Last modification on : Thursday, January 20, 2022 - 4:20:54 PM
Long-term archiving on: : Monday, April 19, 2021 - 6:53:29 PM

File

jlamp2.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Mohamad Jaber, Yliès Falcone, Paul Attie, Al-Abbass Khalil, Rayan Hallal, et al.. From global choreographies to verifiable efficient distributed implementations. Journal of Logical and Algebraic Methods in Programming, Elsevier, 2020, 115, pp.1-24. ⟨10.1016/j.jlamp.2020.100577⟩. ⟨hal-03113398⟩

Share

Metrics

Les métriques sont temporairement indisponibles