Declarative Parameterized Verification of Distributed Protocols via the Cubicle Model Checker - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Fundamenta Informaticae Année : 2021

Declarative Parameterized Verification of Distributed Protocols via the Cubicle Model Checker

Résumé

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.
Fichier non déposé

Dates et versions

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

Identifiants

Citer

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⟩
22 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More