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

Hugues Evrard

Thèse de doctorat de l'Université de Grenoble, Juillet 2015

Résumé:

LNT est un langage formel de spécification récent, basé sur les algèbres de processus, où plusieurs processus concurrents et asynchrones peuvent interagir par rendez-vous multiple, c'est-à-dire à deux ou plus, avec échange de données. La boite à outils CADP (Construction and Analysis of Distributed Processes) offre plusieurs techniques relatives à l'exploration d'espace d'états, comme le model checking, pour vérifier formellement une spécification LNT. Cette thèse présente une méthode de génération d'implémentation distribuée à partir d'un modèle formel LNT décrivant une composition parallèle de processus. En s'appuyant sur CADP, nous avons mis au point le nouvel outil DLC (Distributed LNT Compiler), capable de générer, à partir d'une spécification LNT, une implémentation distribuée en C qui peut ensuite être déployée sur plusieurs machines distinctes reliées par un réseau.

Les implémentations générées nécessitent un protocole de synchronisation pour assurer les rendez-vous multiples avec échange de données entre processus distants. Nous avons mis au point une méthode de vérification de ce type de protocole qui, en utilisant LNT et CADP, permet de vérifier que le protocole réalise, sans introduire ni boucle infinie ni interblocage, des rendez-vous cohérents par rapport à une spécification donnée. Cette méthode nous a permis d'identifier de possibles interblocages dans un protocole de la littérature, que nous avons ensuite corrigé, étendu et amélioré de manière incrémentale, en mettant notre méthode à profit pour vérifier formellement chaque itération. Nous avons aussi développé un mécanisme qui permet, en embarquant au sein d'une implémentation des procédures C librement définies par l'utilisateur, de mettre en place des interactions entre une implémentation générée et d'autres systèmes de son environnement. Enfin, nous avons mesuré les performances des implémentations générées par DLC sur plusieurs exemples, dont un cas d'étude complet sur le nouvel algorithme de consensus Raft.

199 pages

PDF

PostScript

Transparents de la soutenance de thèse de H. Evrard:

PDF