Verifying Declarative Netlog Protocols with Coq: a First Experiment

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.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