Automatic Distributed Code Generation from Formal Models of Asynchronous Processes Interacting by Multiway Rendezvous

Hugues Evrard 1 Frédéric Lang 1
1 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : Formal process languages inheriting the concurrency and communication features of process algebras are convenient formalisms to model distributed applications, especially when they are equipped with formal verification tools (e.g., model checkers) to help hunting for bugs early in the development process. However, even starting from a fully verified formal model, bugs are likely to be introduced while translating (generally by hand) the concurrent model ---which relies on high-level and expressive communication primitives--- into the distributed implementation ---which often relies on low-level communication primitives. In this paper, we present DLC, a compiler that enables distributed code to be generated from models written in a formal process language called LNT, which is equipped with a rich verification toolbox named CADP, and where processes interact by value-passing multiway rendezvous. The generated code uses an elaborate protocol to implement rendezvous, and can be either executed in an autonomous way (i.e., without requiring additional code to be defined by the user), or connected to external software through user-modifiable C functions. The protocol itself is modeled in LNT and verified using CADP. We present several experiments assessing the performance of DLC, including the Raft consensus algorithm.
Type de document :
Article dans une revue
Journal of Logical and Algebraic Methods in Programming, Elsevier, 2016


https://hal.inria.fr/hal-01412911
Contributeur : Frederic Lang <>
Soumis le : vendredi 9 décembre 2016 - 09:14:06
Dernière modification le : jeudi 15 décembre 2016 - 11:19:14

Fichier

Evrard-Lang-16-auteur.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01412911, version 1

Collections

Citation

Hugues Evrard, Frédéric Lang. Automatic Distributed Code Generation from Formal Models of Asynchronous Processes Interacting by Multiway Rendezvous. Journal of Logical and Algebraic Methods in Programming, Elsevier, 2016. <hal-01412911>

Partager

Métriques

Consultations de
la notice

111

Téléchargements du document

33