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.
Declarative parameterized verification of topology-sensitive distributed protocols
Delzanno, Giorgio;Ferrando, Angelo
2019-01-01
Abstract
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.File in questo prodotto:
File | Dimensione | Formato | |
---|---|---|---|
Declarative Parameterized Verification of Topology-Sensitive Distributed Protocols | SpringerLink.pdf
accesso chiuso
Tipologia:
Documento in versione editoriale
Dimensione
509.21 kB
Formato
Adobe PDF
|
509.21 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.