A Framework for Verifying Data-Centric Protocols

Yuxin Deng 1 Stéphane Grumbach 2 Jean-François Monin 3, 4, *
* Auteur correspondant
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
3 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
Abstract : Data centric languages, such as recursive rule based languages, have been proposed to program distributed applications over networks. They simplify greatly the code, while still admitting efficient distributed execution. We show that they also provide a promising approach to the verification of distributed protocols, thanks to their data centric orientation, which allows us to explicitly handle global structures such as the topology of the network. We consider a framework using an original formalization in the Coq proof assistant of a distributed computation model based on message passing with either synchronous or asynchronous behavior. The declarative rules of the Netlog language for specifying distributed protocols and the virtual machines for evaluating these rules are encoded in Coq as well. We consider as a case study tree protocols, and show how this framework enables us to formally verify them in both the asynchronous and synchronous setting.
Type de document :
Communication dans un congrès
Roberto Bruni; Juergen Dingel. 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE), Jun 2011, Reykjavik, Iceland. Springer, Lecture Notes in Computer Science, LNCS-6722, pp.106-120, 2011, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-21461-5_7〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00647802
Contributeur : Jean-François Monin <>
Soumis le : vendredi 2 décembre 2011 - 16:24:51
Dernière modification le : mardi 17 avril 2018 - 11:26:44
Document(s) archivé(s) le : lundi 5 décembre 2016 - 08:41:33

Fichier

vdcp.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Yuxin Deng, Stéphane Grumbach, Jean-François Monin. A Framework for Verifying Data-Centric Protocols. Roberto Bruni; Juergen Dingel. 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE), Jun 2011, Reykjavik, Iceland. Springer, Lecture Notes in Computer Science, LNCS-6722, pp.106-120, 2011, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-21461-5_7〉. 〈hal-00647802〉

Partager

Métriques

Consultations de la notice

574

Téléchargements de fichiers

188