A Framework for Verifying Data-Centric Protocols

Yuxin Deng; Stephane Grumbach; Jean-François Monin

hal-00647802, version 1

A Framework for Verifying Data-Centric Protocols

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

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

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.

a – INRIA
b – Université Joseph Fourier - Grenoble I
1: BASICS (BASICS)
Shanghai Jiaotong University
2: NETQUEST (LIAMA)
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
3: FORMES (LIAMA)
INRIA – Tsinghua University / Beijing – LIAMA
4: Université Joseph Fourier (Grenoble 1 UJF)
Université Joseph Fourier - Grenoble I

hal-00647802, version 1
http://hal.inria.fr/hal-00647802
oai:hal.inria.fr:hal-00647802
From: Jean-François Monin <>
Submitted on: Friday, 2 December 2011 16:24:51
Updated on: Thursday, 8 December 2011 15:39:13

See detailed view

Associated documents

PDF :

DOI: 10.1007/978-3-642-21461-5_7

Export

Bibtex EndNote TEI RefWorks

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="inproceedings"><head>Peer-reviewed conferences/proceedings</head>
<biblStruct type="inproceedings" xml:id="hal-00647802"><analytic>
<author><persName><forename>Yuxin</forename><surname>Deng</surname></persName>
<affiliation>
<orgName type="laboratory">BASICS</orgName>
<orgName type="team">BASICS</orgName>
<country>CN</country>
<orgName type="institution">Shanghai Jiaotong University</orgName>
</affiliation>
</author>
<author><persName><forename>Stephane</forename><surname>Grumbach</surname></persName>
<affiliation>
<orgName type="laboratory">LIAMA</orgName>
<orgName type="team">NETQUEST</orgName>
<country>CN</country>
<orgName type="institution">Centre de coopération internationale en recherche agronomique pour le développement [CIRAD]</orgName>
<orgName type="institution">CNRS</orgName>
<orgName type="institution">Institut national de la recherche agronomique (INRA)</orgName>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">Chinese Academy of Science (CAS)</orgName>
<orgName type="institution">Institute of Automation, Chinese Academy of Sciences</orgName>
</affiliation>
</author>
<author><persName><forename>Jean-François</forename><surname>Monin</surname></persName>
<affiliation>
<orgName type="laboratory">LIAMA</orgName>
<orgName type="team">FORMES</orgName>
<country>CN</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">Tsinghua University / Beijing</orgName>
<orgName type="institution">LIAMA</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">Grenoble 1 UJF</orgName>
<orgName type="team">Université Joseph Fourier</orgName>
<country>FR</country>
<orgName type="institution">Université Joseph Fourier - Grenoble I</orgName>
</affiliation>
</author>
<title type="main" level="a">A Framework for Verifying Data-Centric Protocols</title></analytic><monogr><meeting>DisCoTec 2011 - 6th International Federated Conferences on Formal Techniques for Distributed Systems</meeting><imprint><publisher>Springer</publisher><pubPlace><settlement>Reykjavik</settlement><country>Iceland</country></pubPlace><biblScope type="publicationDate">2011-12-02</biblScope><biblScope type="vol">6722</biblScope><biblScope type="pp">106-120</biblScope></imprint></monogr><idno type="doi">10.1007/978-3-642-21461-5_7</idno><idno type="HALid">http://hal.inria.fr/hal-00647802</idno><idno type="HALFile">http://hal.inria.fr/hal-00647802/PDF/vdcp.pdf</idno></biblStruct>
</listBibl>
</listBibl>