CSP-based counter abstraction for systems with node identifiers
CSP-based counter abstraction for systems with node identifiers
复制标题
DOI：
10.1016/j.scico.2013.03.018
复制
发表时间：
2014-02
期刊：
影响因子：
--
通讯作者：
T. Mazur;G. Lowe
中科院分区：
文献类型：
--
作者：
T. Mazur;G. Lowe
参数化模型检验问题是关于一个实现Im pl（t）是否满足一个规范Spec（t）的问题。在一般情况下，t可以确定许多实体：在网络中使用的进程的数量，数据的类型，缓冲区的容量，等等。本文的主题是自动化的PMCP的一个子类的第一类参数的统一验证，即它确定在网络中使用的进程的数量。我们使用CSP作为我们的形式主义。计数器抽象是一种用抽象状态空间代替具体状态空间的技术，其中每个抽象状态是整数计数器（c 1，...，c k）的元组，使得对于每个i，c i计数当前有多少节点进程处于第i个状态。每个计数器c i都被赋予一个有限的阈值z i，我们将c i= z i解释为在第i个状态中有z i个或多个进程。标准的计数器抽象技术要求所有进程都是相同的，这意味着节点不能使用节点标识符。在本文中，我们提出了如何反抽象技术可以扩展到进程中，使节点标识符的对称方式使用。我们的方法创建了一个过程A B s t r，它与t无关，并且对于所有足够大的T，它由（I m p l（T））细化，其中将参数的所有（足够大的）实例化T映射到某个固定类型。通过加细的传递性，测试A B st r是否加细Spec（t）意味着Spec（t））被加细Iim pl（T）。然后，使用Mazur和Lowe（2012）[29]的类型约简理论，我们可以推导出对于所有足够大的T，S p e c（T）被I m p l（T）精化，从而获得原始验证问题的肯定答案。
Abstract The Parameterised Model Checking Problem asks whether an implementation I m p l (t) satisfies a specification S p e c (t) for all instantiations of parameter t. In general, t can determine numerous entities: the number of processes used in a network, the type of data, the capacities of buffers, etc. The main theme of this paper is automation of uniform verification of a subclass of PMCP with the parameter of the first kind, ie where it determines the number of processes used in a network. We use CSP as our formalism. Counter abstraction is a technique that replaces a concrete state space by an abstract one, where each abstract state is a tuple of integer counters (c 1,…, c k) such that for each i, c i counts how many node processes are currently in the i-th state. Each counter c i is given a finite threshold z i and we interpret c i= z i as there being z i or more processes in the i-th state. Standard counter abstraction techniques require all processes to be identical, which means that nodes cannot use node identifiers. In this paper we present how counter abstraction techniques can be extended to processes that make use of node identifiers in a symmetrical way. Our method creates a process A b s t r that is independent of t and is refined by ϕ (I m p l (T)) for all sufficiently large T, where ϕ maps all (sufficiently large) instantiations T of the parameter to some fixed type. By transitivity of refinement, testing if A b s t r refines S p e c (ϕ (t)) implies that S p e c (ϕ (t)) is refined by ϕ (I m p l (T)). Then, using the type reduction theory from Mazur and Lowe (2012)[29], we can deduce that S p e c (T) is refined by I m p l (T) for all sufficiently large T, thus obtaining a positive answer to the original verification problem.