hal-00647802, version 1

A Framework for Verifying Data-Centric Protocols

Yuxin Deng () ¹, Stephane Grumbach () ^a, 2, Jean-François Monin (, ) ^b, 3, 4

DisCoTec 2011 - 6th International Federated Conferences on Formal Techniques for Distributed Systems 6722 (2011) 106-120

• a –  INRIA
• b –  Université Joseph Fourier - Grenoble I
• 1 :  BASICS (BASICS)
• http://basics.sjtu.edu.cn
  Shanghai Jiaotong University Department of Computer Science School of Electronics and Informatics Shanghai Jiaotong University 800 Dongchuan Road Shanghai 200240 China Chine
• 2 :  NETQUEST (LIAMA)
• http://liama.ia.ac.cn/
  Centre de coopération internationale en recherche agronomique pour le développement [CIRAD] – CNRS – Institut national de la recherche agronomique (INRA) – INRIA – Chinese Academy of Science (CAS) – Institute of Automation, Chinese Academy of Sciences Institut d'Automatique - Académie des Sciences de Chine PO Box 2728 - Beijing 100080 R. P. Chine Tél. : (+ 86 10) 62 64 74 59 Fax : (+ 86 10) 62 64 74 58 Chine
• 3 :  FORMES (LIAMA)
• http://liama.ia.ac.cn/wiki/projects:formes:home
  INRIA – Tsinghua University / Beijing – LIAMA Tsinghua University FIT Building Haidian District 100084 Beijing China Chine
• 4 :  Université Joseph Fourier (Grenoble 1 UJF)
• http://www.ujf-grenoble.fr/
  Université Joseph Fourier - Grenoble I Université Joseph Fourier - BP 53 - 38041 Grenoble Cedex 9 France

Références bibliographiques

• Type de publication : Communications avec actes
• Domaine : Informatique/Calcul parallèle, distribué et partagé
• Titre : A Framework for Verifying Data-Centric Protocols
• Résumé : 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.
• Langue du document : Anglais
• Date de publication : 02/12/2011
• Audience : internationale
• Titre conférence : DisCoTec 2011 - 6th International Federated Conferences on Formal Techniques for Distributed Systems
• Ville : Reykjavik
• Pays : Islande
• Date conférence : 06/06/2011
• Date conférence (fin) : 09/06/2011
• Editeur(s) scientifique(s) : Bruni, Roberto and Dingel, Juergen
• Editeur commercial : Springer
• Titre volume : Formal Techniques for Distributed Systems
• Volume : 6722
• Collection : Lecture Notes in Computer Science
• Pagination : 106-120
• DOI : 10.1007/978-3-642-21461-5_7

Liste des fichiers attachés à ce document :

• hal-00647802, version 1
• http://hal.inria.fr/hal-00647802
• oai:hal.inria.fr:hal-00647802
• Contributeur : Jean-François Monin <>
• Soumis le : Vendredi 2 Décembre 2011, 16:24:51
• Dernière modification le : Jeudi 8 Décembre 2011, 15:39:13