Logic-based Verification of the Distributed Dining Philosophers Protocol

Issue title: Special Issue on the 31Th Italian Conference on Computational Logic: CILC 2016

Guest editors: Camillo Fiorentini, Alberto Momigliano and Alberto Pettorossi

Article type: Research Article

Authors: Delzanno, Giorgio^{; *}

Affiliations: DIBRIS, University of Genova, Italy. giorgio.delzanno@unige.it

Correspondence: [*] Address for correspondence: DIBRIS, University of Genova, Italy

Abstract: We present a logic-based framework for the specification and validation of distributed protocols. Our specification language is a logic-based presentation of update rules for arbitrary graphs. Update rules are specified via conditional rewriting rules defined over a relational language. We focus our attention on unary and binary relations as a way to specify predicates over nodes and edges of a graph. For the considered language, we define assertions that can be applied to specify correctness properties for arbitrary configurations. We apply the language to model the distributed version of the Dining Philosopher Protocol. The protocol is defined for asynchronous processes distributed over a graph with arbitrary topology. We propose then validation methods based on source to source transformations and deductive reasoning. We apply the resulting method to provide a succint correctness proof of the considered case-study.

DOI: 10.3233/FI-2018-1697

Journal: Fundamenta Informaticae, vol. 161, no. 1-2, pp. 113-133, 2018