Parameterised verification of randomised distributed systems using state-based models
Parameterised verification of randomised distributed systems using state-based models
复制标题
使用基于状态的模型对随机分布式系统进行参数化验证
DOI：
10.5591/978-1-57735-516-8/ijcai11-279
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
Douglas Graham
中科院分区：
文献类型：
--
作者：
Douglas Graham
模型检查是验证分布式系统的强大技术，但仅限于验证具有固定数量进程的系统。对任意数量进程的系统验证称为参数化模型检查问题，并且通常是不可判定的。针对非概率分布式系统，参数化模型检查已得到深入研究。我们扩展了其中的一些工作，以解决表现出概率行为的分布式协议的参数化模型检查问题，该问题迄今为止尚未得到广泛解决。
特别是，我们考虑将网络不变量和显式归纳法应用于随机分布式系统基于状态的模型的参数化验证。我们通过为简单计数器令牌环协议的非概率和概率形式构建不变模型来演示网络不变量的使用。我们证明，证明不变量的属性等同于证明任意数量进程的令牌环协议的属性。
考虑使用归纳法来验证一类随机分布式系统。这些系统被称为退化系统，具有这样的特性：具有给定通信图的系统模型最终表现得像具有简化图的系统模型，其中简化是通过删除一组节点来实现的。我们根据系统退化的方式来区分确定性系统、概率性系统和半退化系统。对于前两类，我们描述了归纳模式，用于在任意通信图上推理这些系统的模型。我们证明，如果某些属性适用于具有某些基本图的系统的所有模型，则它们适用于具有任何图的此类系统的模型，并通过案例研究证明了这一点：两个随机领导者选举协议。我们通过考虑一个简单的八卦协议来说明如何使用归纳法来证明半退化系统的属性。
Model checking is a powerful technique for the verification of distributed systems but is limited to verifying systems with a fixed number of processes. The verification of a system for an arbitrary number of processes is known as the parameterised model checking problem and is, in general, undecidable. Parameterised model checking has been studied in depth for non-probabilistic distributed systems. We extend some of this work in order to tackle the parameterised model checking problem for distributed protocols that exhibit probabilistic behaviour, a problem that has not been widely addressed to date.
In particular, we consider the application of network invariants and explicit induction to the parameterised verification of state-based models of randomised distributed systems. We demonstrate the use of network invariants by constructing invariant models for non-probabilistic and probabilistic forms of a simple counter token ring protocol. We show that proving properties of the invariants equates to proving properties of the token ring protocol for any number of processes.
The use of induction is considered for the verification of a class of randomised distributed systems. These systems, termed degenerative, have the property that a model of a system with given communication graph eventually behaves like a model of a system with a reduced graph, where reduction is by removal of a set of nodes. We distinguish between deterministically, probabilistically and semi-degenerative systems, according to the manner in which a system degenerates. For the former two classes we describe induction schemas for reasoning about models of these systems over arbitrary communication graphs. We show that certain properties hold for models of such systems with any graph if they hold for all models of a system with some base graph and demonstrate this via case studies: two randomised leader election protocols. We illustrate how induction can also be employed to prove properties of semi-degenerative systems by considering a simple gossip protocol.