We present a framework for the specification of distributed protocols based on a logic-based presentation of bipartite graphs. For the considered language, we define assertions that can be applied to 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. To validate the protocol, we apply permutation schemes, transformation rules, and inductive verification.
A Logic-based approach to verify distributed protocols
Delzanno, Giorgio
2016-01-01
Abstract
We present a framework for the specification of distributed protocols based on a logic-based presentation of bipartite graphs. For the considered language, we define assertions that can be applied to 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. To validate the protocol, we apply permutation schemes, transformation rules, and inductive verification.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
