From global choreographies to verifiable efficient distributed implementations - Archive ouverte HAL Access content directly
Journal Articles Journal of Logical and Algebraic Methods in Programming Year : 2020

From global choreographies to verifiable efficient distributed implementations

(1) , (2, 3) , (4) , (1) , (1) , (3)
1
2
3
4

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.
Fichier principal
Vignette du fichier
jlamp2.pdf (558.02 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03113398 , version 1 (18-01-2021)

Identifiers

Cite

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, 2020, 115, pp.1-24. ⟨10.1016/j.jlamp.2020.100577⟩. ⟨hal-03113398⟩
37 View
186 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More