Declarative Parameterized Verification of Distributed Protocols via the Cubicle Model Checker - Archive ouverte HAL Access content directly
Journal Articles Fundamenta Informaticae Year : 2021

Declarative Parameterized Verification of Distributed Protocols via the Cubicle Model Checker

(1) , (2) , (3)
1
2
3

Abstract

We show that Cubicle, an SMT-based infinite-state model checker, can be applied as a verification engine for GLog, a logic-based language based on relational updates rules that has been applied to specify topology-sensitive distributed protocols with asynchronous communication. In this setting, the absence of protocol anomalies can be reduced to a coverability problem in which the initial set of configurations is not fixed a priori (Existential Coverability Problem). Existential Coverability in GLog can naturally be expressed into Parameterized Verification judgements in Cubicle. The encoding is based on a translation of relational update rules into transition rules that modify cells of unbounded arrays. To show the effectiveness of the approach, we discuss several verification problems for distributed protocols and distributed objects, a challenging task for traditional verification tools. The experimental results show the flexibility and robustness of Cubicle for the considered class of protocol examples.
Not file

Dates and versions

hal-03476675 , version 1 (13-12-2021)

Identifiers

Cite

Sylvain Conchon, Giorgio Delzanno, Angelo Ferrando. Declarative Parameterized Verification of Distributed Protocols via the Cubicle Model Checker. Fundamenta Informaticae, 2021, 178 (4), pp.347-378. ⟨10.3233/FI-2021-2010⟩. ⟨hal-03476675⟩
16 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More