From global choreographies to verifiable efficient distributed implementations
| Autor: | Mohamad Y. Jaber, Rayan Hallal, Al-Abbass Khalil, Antoine El-Hokayem, Paul C. Attie, Yliès Falcone |
|---|---|
| Přispěvatelé: | American University of Beirut [Beyrouth] (AUB), Université Grenoble Alpes - UFR Informatique, mathématiques et mathématiques appliquées (UGA UFR IM2AG), Université Grenoble Alpes (UGA), Compiler Optimization and Run-time Systems (CORSE), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire d'Informatique de Grenoble (LIG), Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Augusta University, University System of Georgia (USG), Université Grenoble Alpes - UFR Informatique et Mathématiques Appliquées (UGA UFR IMAG) |
| Jazyk: | angličtina |
| Rok vydání: | 2020 |
| Předmět: |
Java
LOOP (programming language) Logic Computer science Distributed computing 0102 computer and information sciences [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] Translation (geometry) 01 natural sciences Theoretical Computer Science Choreography Set (abstract data type) Computational Theory and Mathematics Promela 010201 computation theory & mathematics Verifiable secret sharing [INFO.INFO-ES]Computer Science [cs]/Embedded Systems computer Implementation Software computer.programming_language |
| Zdroj: | Journal of Logical and Algebraic Methods in Programming Journal of Logical and Algebraic Methods in Programming, 2020, 115, pp.1-24. ⟨10.1016/j.jlamp.2020.100577⟩ Journal of Logical and Algebraic Methods in Programming, Elsevier, 2020, 115, pp.1-24. ⟨10.1016/j.jlamp.2020.100577⟩ |
| ISSN: | 2352-2208 |
| DOI: | 10.1016/j.jlamp.2020.100577⟩ |
| Popis: | International audience; 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect