A Framework for Verifying Data-Centric Protocols

International audience 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 t...

Full description

Bibliographic Details
Main Authors: Deng, Yuxin, Grumbach, Stéphane, Monin, Jean-François
Other Authors: BASICS (BASICS), Shanghai Jiao Tong University Shanghai, NETQUEST (NETQUEST), Centre de Coopération Internationale en Recherche Agronomique pour le Développement (Cirad)-Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de la Recherche Agronomique (INRA)-Chinese Academy of Sciences Changchun Branch (CAS)-Institute of Automation - Chinese Academy of Sciences-Centre National de la Recherche Scientifique (CNRS), Formal Methods for Embedded Systems (FORMES), Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées (LIAMA), Centre de Coopération Internationale en Recherche Agronomique pour le Développement (Cirad)-Institut National de la Recherche Agronomique (INRA)-Chinese Academy of Sciences Changchun Branch (CAS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Institute of Automation - Chinese Academy of Sciences-Centre National de la Recherche Scientifique (CNRS)-Centre de Coopération Internationale en Recherche Agronomique pour le Développement (Cirad)-Institut National de la Recherche Agronomique (INRA)-Chinese Academy of Sciences Changchun Branch (CAS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Institute of Automation - Chinese Academy of Sciences-Centre National de la Recherche Scientifique (CNRS)-Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria), Université Joseph Fourier - Grenoble 1 (UJF), Roberto Bruni, Juergen Dingel, TC 6, WG 6.1
Format: Conference Object
Language:English
Published: HAL CCSD 2011
Subjects:
Online Access:https://inria.hal.science/hal-00647802
https://inria.hal.science/hal-00647802/document
https://inria.hal.science/hal-00647802/file/vdcp.pdf
https://doi.org/10.1007/978-3-642-21461-5_7
Description
Summary:International audience 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.