Génération automatique d'implémentation distribuée à partir de modèles formels de processus concurrents asynchrones

Abstract : LNT is a recent formal specification language, based on process algebras, where several concurrent asynchronous processes can interact by multiway rendezvous (i.e., involving two or more processes), with data exchange. The CADP (Construction and Analysis of Distributed Processes) toolbox offers several techniques related to state space exploration, like model checking, to formally verify an LNT specification. This thesis introduces a distributed implementation generation method, starting from an LNT formal model of a parallel composition of processes. Taking advantage of CADP, we developed the new DLC (Distributed LNT Compiler) tool, which is able to generate, from an LNT specification, a distributed implementation in C that can be deployed on several distinct machines linked by a network. In order to handle multiway rendezvous with data exchange between distant processes in a correct and efficient manner, we designed a synchronization protocol that gathers different approaches suggested in the past. We set up a verification method for this kind of protocol, which, using LNT and CADP, can detect livelocks or deadlocks due to the protocol, and also check that the protocol leads to valid interactions with respect to a given specification. This method allowed us to identify possible deadlocks in a protocol from the literature, and to verify the good behavior of our own protocol. We also designed a mechanism that enables the final user, by embedding user-defined C procedures into the implementation, to set up interactions between the generated implementation and other systems in the environment. Finally, we used the new consensus algorithm Raft as a case study, in particular to measure the performances of an implementation generated by DLC.
Liste complète des métadonnées

Cited literature [70 references]  Display  Hide  Download

https://hal.inria.fr/tel-01215634
Contributor : Frederic Lang <>
Submitted on : Wednesday, October 14, 2015 - 3:44:12 PM
Last modification on : Saturday, December 16, 2017 - 3:34:36 AM
Document(s) archivé(s) le : Friday, January 15, 2016 - 1:10:40 PM

Identifiers

  • HAL Id : tel-01215634, version 1

Citation

Hugues Evrard. Génération automatique d'implémentation distribuée à partir de modèles formels de processus concurrents asynchrones. Génie logiciel [cs.SE]. Université Grenoble Alpes, 2015. Français. 〈NNT : 2015GREAM020〉. 〈tel-01215634〉

Share

Metrics

Record views

577

Files downloads

524