Parameterized Verification of Topology-sensitive Distributed Protocols goes Declarative

Abstract : We show that Cubicle, an SMT-based infinite-state model checker, can be applied as a verification engine for GLog, a logic-based specification language for topology-sensitive distributed protocols with asynchronous communication. Existential coverability queries in GLog can be translated into verification judgements in Cubicle by encoding relational updates rules as unbounded array transitions. We apply the resulting framework to automatically verify a distributed version of the Dining Philosopher mutual exclusion protocol formulated for an arbitrary number of nodes and communication buffers.
Document type :
Conference papers
Complete list of metadatas

Cited literature [19 references]  Display  Hide  Download

https://hal.inria.fr/hal-02001652
Contributor : Sylvain Conchon <>
Submitted on : Thursday, January 31, 2019 - 11:53:42 AM
Last modification on : Friday, January 10, 2020 - 1:33:20 AM
Long-term archiving on: Wednesday, May 1, 2019 - 3:16:30 PM

File

main-2.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02001652, version 1

Citation

Sylvain Conchon, Giorgio Delzanno, Angelo Ferrando. Parameterized Verification of Topology-sensitive Distributed Protocols goes Declarative. International Conference on Networked Systems (NETYS), May 2018, Essaouira, Morocco. ⟨hal-02001652⟩

Share

Metrics

Record views

31

Files downloads

125