Towards Verifying Declarative Netlog Protocols with Coq

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 : Declarative languages, such as recursive rule based languages, have been proposed to program distributed applications over networks.It has been shown that they simplify greatly the code, while still offering efficient distributed execution. In this paper, we show that moreover they provide a promising approach to the verification of distributed protocols. We choose the Netlog language and use the Coq proof assistant. We first formalize the distributed computation model based on message passing with either synchronous or asynchronous behavior. We then see how the declarative rules of the protocols can be simply encoded in Coq. Finally, we develop the machine embedded on each node of the network which evaluates the rules. This framework enables us to formally verify distributed declarative protocols, as sketched on a concrete example, a breadth-first search tree construction in a distributed network.
Type de document :
Rapport
[Intern report] 2010, pp.20
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00506093
Contributeur : Jean-François Monin <>
Soumis le : mardi 27 juillet 2010 - 10:46:35
Dernière modification le : jeudi 11 janvier 2018 - 06:22:29
Document(s) archivé(s) le : mardi 23 octobre 2012 - 11:26:22

Fichier

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

Identifiants

  • HAL Id : inria-00506093, version 1

Collections

Citation

Yuxin Deng, Stéphane Grumbach, Jean-François Monin. Towards Verifying Declarative Netlog Protocols with Coq. [Intern report] 2010, pp.20. 〈inria-00506093〉

Partager

Métriques

Consultations de la notice

383

Téléchargements de fichiers

137