Declarative Parameterized Verification of Distributed Protocols via the Cubicle Model Checker

2021 ◽  
Vol 178 (4) ◽  
pp. 347-378
Author(s):  
Sylvain Conchon ◽  
Giorgio Delzanno ◽  
Angelo Ferrando
Keyword(s):  
A Priori ◽  
Asynchronous Communication ◽  
Model Checker ◽  
Distributed Objects ◽  
Distributed Protocols ◽  
Parameterized Verification ◽  
Verification Tools ◽  
Transition Rules ◽  
Update Rules ◽  
Infinite State

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.

scholarly journals Reachability Modulo Theory Library

10.29007/f3rp ◽  
2018 ◽  
Author(s):  
Francesco Alberti ◽  
Roberto Bruttomesso ◽  
Silvio Ghilardi ◽  
Silvio Ranise ◽  
Natasha Sharygina
Keyword(s):  
Reachability Analysis ◽  
Safety Properties ◽  
Standard Language ◽  
Transition Systems ◽  
Smt Solvers ◽  
Verification Tools ◽  
Infinite State Systems ◽  
Infinite State

Reachability analysis of infinite-state systems plays a central role in many verification tasks. In the last decade, SMT-Solvers have been exploited within many verification tools to discharge proof obligations arising from reachability analysis. Despite this, as of today there is no standard language to deal with transition systems specified in the SMT-LIB format. This paper is a first proposal for a new SMT-based verification language that is suitable for defining transition systems and safety properties.

SMT-based verification of data-aware processes: a model-theoretic approach

2020 ◽  
Vol 30 (3) ◽  
pp. 271-313
Author(s):  
Diego Calvanese ◽  
Silvio Ghilardi ◽  
Alessandro Gianola ◽  
Marco Montali ◽  
Andrey Rivkin
Keyword(s):  
Model Theory ◽  
Satisfiability Modulo Theories ◽  
Theoretic Approach ◽  
Model Checker ◽  
Present Contribution ◽  
Relational Systems ◽  
Infinite State Systems ◽  
Algorithmic Techniques ◽  
The One ◽  
Infinite State

AbstractIn recent times, satisfiability modulo theories (SMT) techniques gained increasing attention and obtained remarkable success in model-checking infinite-state systems. Still, we believe that whenever more expressivity is needed in order to specify the systems to be verified, more and more support is needed from mathematical logic and model theory. This is the case of the applications considered in this paper: we study verification over a general model of relational, data-aware processes, to assess (parameterized) safety properties irrespectively of the initial database (DB) instance. Toward this goal, we take inspiration from array-based systems and tackle safety algorithmically via backward reachability. To enable the adoption of this technique in our rich setting, we make use of the model-theoretic machinery of model completion, which surprisingly turns out to be an effective tool for verification of relational systems and represents the main original contribution of this paper. In this way, we pursue a twofold purpose. On the one hand, we isolate three notable classes for which backward reachability terminates, in turn witnessing decidability. Two of such classes relate our approach to conditions singled out in the literature, whereas the third one is genuinely novel. On the other hand, we are able to exploit SMT technology in implementations, building on the well-known MCMT (Model Checker Modulo Theories) model checker for array-based systems and extending it to make all our foundational results fully operational. All in all, the present contribution is deeply rooted in the long-standing tradition of the application of model theory in computer science. In particular, this paper applies these ideas in an original mathematical context and shows how these techniques can be used for the first time to empower algorithmic techniques for the verification of infinite-state systems based on arrays, so as to make such techniques applicable to the timely, challenging settings of data-aware processes.

scholarly journals STAMINA: STochastic Approximate Model-Checker for INfinite-State Analysis

2019 ◽  
pp. 540-549 ◽  
Author(s):  
Thakur Neupane ◽  
Chris J. Myers ◽  
Curtis Madsen ◽  
Hao Zheng ◽  
Zhen Zhang
Keyword(s):  
Approximate Model ◽  
Model Checker ◽  
Infinite State ◽  
State Analysis

scholarly journals INFAMY: An Infinite-State Markov Model Checker

2009 ◽  
pp. 641-647 ◽  
Author(s):  
Ernst Moritz Hahn ◽  
Holger Hermanns ◽  
Björn Wachter ◽  
Lijun Zhang
Keyword(s):  
Markov Model ◽  
Model Checker ◽  
Infinite State

Approximated parameterized verification of infinite-state processes with global conditions

2008 ◽  
Vol 34 (2) ◽  
pp. 126-156 ◽  
Author(s):  
Parosh Aziz Abdulla ◽  
Giorgio Delzanno ◽  
Ahmed Rezine
Keyword(s):  
Parameterized Verification ◽  
Infinite State

Binary Adaptive Ant Colony Optimization in Reactive Power Optimization

2012 ◽  
Vol 616-618 ◽  
pp. 2091-2096 ◽  
Author(s):  
Hong Hong ◽  
Fang Liu
Keyword(s):  
Ant Colony Optimization ◽  
State Transition ◽  
Reactive Power ◽  
Ant Colony ◽  
Reactive Power Optimization ◽  
Ant Colony Optimization Algorithm ◽  
Information Update ◽  
Transition Rules ◽  
Update Rules ◽  
State Transition Rules

This article proposed an Adaptive Binary Ant Colony Optimization Algorithm, which is based on the dual network diagram, designed to state transition rules and information update rules, and then according to the algorithm processes adjust information volatilizing factor dynamically, Verify the validity and superiority of the algorithm.

scholarly journals A Multistep Extending Truncation Method towards Model Construction of Infinite-State Markov Chains

2014 ◽  
Vol 2014 ◽  
pp. 1-6
Author(s):  
Kemin Wang ◽  
Yongbin Wang ◽  
Zhengtao Jiang ◽  
Wenlong Fu
Keyword(s):  
Model Checking ◽  
Markov Chains ◽  
Continuous Time ◽  
Model Construction ◽  
Model Checker ◽  
State Explosion ◽  
Truncation Method ◽  
Continuous Time Markov Chains ◽  
System Properties ◽  
Infinite State

The model checking of Infinite-State Continuous Time Markov Chains will inevitably encounter the state explosion problem when constructing the CTMCs model; our method is to get a truncated model of the infinite one; to get a sufficient truncated model to meet the model checking of Continuous Stochastic Logic based system properties, we propose a multistep extending advanced truncation method towards model construction of CTMCs and implement it in the INFAMY model checker; the experiment results show that our method is effective.

scholarly journals Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems

2021 ◽  
pp. 529-551
Author(s):  
Sergio Mover ◽  
Alessandro Cimatti ◽  
Alberto Griggio ◽  
Ahmed Irfan ◽  
Stefano Tonetta
Keyword(s):  
Dynamical Systems ◽  
Discrete Systems ◽  
Model Checker ◽  
Safety Verification ◽  
Polynomial Dynamical Systems ◽  
Main Challenge ◽  
Safety Property ◽  
Verification Problem ◽  
Explicit Enumeration ◽  
Infinite State

AbstractSemi-algebraic abstraction is an approach to the safety verification problem for polynomial dynamical systems where the state space is partitioned according to the sign of a set of polynomials. Similarly to predicate abstraction for discrete systems, the number of abstract states is exponential in the number of polynomials. Hence, semi-algebraic abstraction is expensive to explicitly compute and then analyze (e.g., to prove a safety property or extract invariants).In this paper, we propose an implicit encoding of the semi-algebraic abstraction, which avoids the explicit enumeration of the abstract states: the safety verification problem for dynamical systems is reduced to a corresponding problem for infinite-state transition systems, allowing us to reuse existing model-checking tools based on Satisfiability Modulo Theory (SMT). The main challenge we solve is to express the semi-algebraic abstraction as a first-order logic formula that is linear in the number of predicates, instead of exponential, thus letting the model checker lazily explore the exponential number of abstract states with symbolic techniques. We implemented the approach and validated experimentally its potential to prove safety for polynomial dynamical systems.

Sign in / Sign up

Export Citation Format

Share Document