Parameterized verification of coverability in infinite state broadcast networks

2020 ◽  
pp. 104592
Author(s):  
A.R. Balasubramanian
Keyword(s):  
Broadcast Networks ◽  
Parameterized Verification ◽  
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

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 An Automatic Proving Approach to Parameterized Verification

2018 ◽  
Vol 19 (4) ◽  
pp. 1-25 ◽  
Author(s):  
Yongjian Li ◽  
Kaiqiang Duan ◽  
David N. Jansen ◽  
Jun Pang ◽  
Lijun Zhang ◽  
...  
Keyword(s):  
Parameterized Verification

Insensitivity of steady-state distributions of generalized semi-Markov processes by speeds

1978 ◽  
Vol 10 (04) ◽  
pp. 836-851 ◽  
Author(s):  
R. Schassberger
Keyword(s):  
Steady State ◽  
General System ◽  
State Distribution ◽  
Lifetime Distributions ◽  
State Dependent ◽  
Semi Markov Process ◽  
Semi Markov Processes ◽  
Infinite State ◽  
State Case ◽  
Residual Lifetimes

A generalized semi-Markov process with speeds describes the fluctuation, in time, of the state of a certain general system involving, at any given time, one or more living components, whose residual lifetimes are being reduced at state-dependent speeds. Conditions are given for the stationary state distribution, when it exists, to depend only on the means of some of the lifetime distributions, not their exact shapes. This generalizes results of König and Jansen, particularly to the infinite-state case.

Sign in / Sign up

Export Citation Format

Share Document