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 / Conchon, Sylvain; Delzanno, Giorgio; Ferrando, Angelo. - (2019), pp. 209-224. (Intervento presentato al convegno 6th International Conference on Networked Systems, NETYS 2018 tenutosi a Essaouira, Morocco nel 9 maggio 2018) [10.1007/978-3-030-05529-5_14].

Declarative parameterized verification of topology-sensitive distributed protocols

Ferrando, Angelo
2019

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.
2019
6th International Conference on Networked Systems, NETYS 2018
Essaouira, Morocco
9 maggio 2018
209
224
Conchon, Sylvain; Delzanno, Giorgio; Ferrando, Angelo
Declarative parameterized verification of topology-sensitive distributed protocols / Conchon, Sylvain; Delzanno, Giorgio; Ferrando, Angelo. - (2019), pp. 209-224. (Intervento presentato al convegno 6th International Conference on Networked Systems, NETYS 2018 tenutosi a Essaouira, Morocco nel 9 maggio 2018) [10.1007/978-3-030-05529-5_14].
File in questo prodotto:
File Dimensione Formato  
Declarative Parameterized Verification of Topology-Sensitive Distributed Protocols | SpringerLink.pdf

Accesso riservato

Dimensione 509.21 kB
Formato Adobe PDF
509.21 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
Pubblicazioni consigliate

Licenza Creative Commons
I metadati presenti in IRIS UNIMORE sono rilasciati con licenza Creative Commons CC0 1.0 Universal, mentre i file delle pubblicazioni sono rilasciati con licenza Attribuzione 4.0 Internazionale (CC BY 4.0), salvo diversa indicazione.
In caso di violazione di copyright, contattare Supporto Iris

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11380/1331825
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? ND
social impact