Verifying Declarative Netlog Protocols with Coq: a First ExperimentReportar como inadecuado




Verifying Declarative Netlog Protocols with Coq: a First Experiment - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 CSE - Department of Computer Science and Engineering Shanghai 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 Science , Institute of Automation - Chinese Academy of Sciences, CNRS - Centre National de la Recherche Scientifique 3 UJF - Université Joseph Fourier - Grenoble 1

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 report, we show that moreover they provide a promising approach to the verification of distributed protocols. We consider 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 and we develop the machine embedded on each node of the network which evaluates the rules. This framework enables us to formally verify distributed protocols, as shown on a concrete case study, a spanning tree construction in both the asynchronous and synchronous setting.

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.





Autor: Yuxin Deng - Stéphane Grumbach - Jean-François Monin -

Fuente: https://hal.archives-ouvertes.fr/



DESCARGAR PDF




Documentos relacionados