Declarative parameterized verification of topology-sensitive distributed protocols

Conchon, S, Delzanno, G and Ferrando, A ORCID: 0000-0002-8711-4670 (2019) Declarative parameterized verification of topology-sensitive distributed protocols. .

Text HCVS_2018_paper_2.pdf - Author Accepted Manuscript Download (283kB)

Abstract

© Springer Nature Switzerland AG 2019. We show that Cubicle [9], 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.

Item Type:	Conference or Workshop Item (Unspecified)
Depositing User:	Symplectic Admin
Date Deposited:	11 Feb 2019 09:04
Last Modified:	19 Jan 2023 01:04
DOI:	10.1007/978-3-030-05529-5_14
Related URLs:	Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3032627