A Framework for Verifying Data-Centric Protocols

12 years 8 months ago
A Framework for Verifying Data-Centric Protocols
Abstract. Data centric languages, such as recursive rule based languages, have been proposed to program distributed applications over networks. They simplify greatly the code, which is orders of magnitude shorter, much more declarative, 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 to explicitly handle global structures, such as the topology of the network, routing tables, trees, etc, as well as their properties. 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, as well as the virtual machines for evaluating these rules, are encoded in Coq as well. We consider as a case study tree protocols, and show how...
Yuxin Deng, Stéphane Grumbach, Jean-Fran&cc
Added 28 Aug 2011
Updated 28 Aug 2011
Type Journal
Year 2011
Authors Yuxin Deng, Stéphane Grumbach, Jean-François Monin
Comments (0)