Verifying Declarative Netlog Protocols with Coq: a First Experiment

Yuxin Deng 1 Stéphane Grumbach 2 Jean-François Monin 3
2 NETQUEST - NETQUEST
CIRAD - Centre de Coopération Internationale en Recherche Agronomique pour le Développement, Inria Paris-Rocquencourt, INRA - Institut National de la Recherche Agronomique, CAS - Chinese Academy of Sciences [Changchun Branch], Institute of Automation - Chinese Academy of Sciences, CNRS - Centre National de la Recherche Scientifique
Résumé : L'idée d'utiliser des langages déclaratifs, par exemple à base de règles récursives, a été proposée pour programmer des applications distribuées sur des réseaux. Il a été montré que cela simplifie grandement le code, sans sacrifier l'efficacité de l'exécution distribuée. Dans ce rapport, nous montrons qu'en outre ils constituent une approche prometteuse à la vérification de protocoles. Nous considérons le langage Netlog et utilisons l'assistant à la preuve Coq. Nous commençons par formaliser le modèle de calcul distribué par communication de message dans les deux variantes synchrone et asynchrone. Nous montrons ensuite un encodage simple en Coq des règles définissant un protocole et ainsi que de leur évaluation sur chaque noeud du réseau. Ce cadre permet de vérifier formellement des protocoles distribués, comme illustré sur une étude de cas concrète, la construction d'un arbre, tant dans le cas synchrone que dans le cas asynchrone.
Type de document :
Rapport
[Research Report] RR-7511, INRIA. 2011
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00567811
Contributeur : Stephane Grumbach <>
Soumis le : mardi 22 février 2011 - 01:17:39
Dernière modification le : jeudi 11 janvier 2018 - 06:21:19
Document(s) archivé(s) le : mardi 6 novembre 2012 - 14:40:17

Fichier

RR-7511.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00567811, version 1

Collections

Citation

Yuxin Deng, Stéphane Grumbach, Jean-François Monin. Verifying Declarative Netlog Protocols with Coq: a First Experiment. [Research Report] RR-7511, INRIA. 2011. 〈inria-00567811〉

Partager

Métriques

Consultations de la notice

360

Téléchargements de fichiers

204