Automatic Distributed Code Generation from Formal Models of Asynchronous Concurrent Processes

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. The generated code 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. We present an experiment where DLC generates a distributed implementation from the LNT model of the Raft consensus algorithm.
Type de document :
Communication dans un congrès
23rd Euromicro International Conference on Parallel, Distributed and Network-based Processing (PDP 2015), Mar 2015, Turku, Finland. 2015, 〈http://www.pdp2015.org〉
Liste complète des métadonnées

Littérature citée [38 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01086522
Contributeur : <>
Soumis le : vendredi 5 juin 2015 - 16:24:24
Dernière modification le : mercredi 14 décembre 2016 - 01:08:45
Document(s) archivé(s) le : mardi 15 septembre 2015 - 11:42:36

Licence


Distributed under a Creative Commons Paternité - Pas d'utilisation commerciale 4.0 International License

Identifiants

  • HAL Id : hal-01086522, version 1
  • Mot de passe : m6g863xr

Collections

Citation

Hugues Evrard, Frédéric Lang. Automatic Distributed Code Generation from Formal Models of Asynchronous Concurrent Processes. 23rd Euromicro International Conference on Parallel, Distributed and Network-based Processing (PDP 2015), Mar 2015, Turku, Finland. 2015, 〈http://www.pdp2015.org〉. 〈hal-01086522〉

Partager

Métriques

Consultations de la notice

2125

Téléchargements de fichiers

586