具有无复位阵列的数据无关系统的模型检验
On model checking data-independent systems with arrays without reset
摘要：
一个系统对于一个数据类型X是数据独立的，当它可以对类型X的值执行的操作仅限于相等性测试。系统还可以存储、输入和输出类型X的值。我们研究的模型检验的系统是数据独立的两个不同的类型变量X和Y，并可能另外使用数组的索引从X和值从Y。我们的主要兴趣是下面的参数化模型检查问题：一个给定的程序是否满足一个给定的时间逻辑公式的所有非空的nite实例的X和Y。最初，我们考虑的抽象，而不是X和Y是无限的，其中部分功能与有限域被用来模拟阵列。使用一个翻译的数据无关的系统，没有数组，我们表明，u演算模型检查问题是可判定的这些系统。从这个结果，我们可以推出所有系统的性质与有限的情况下，X和Y。我们表明，有一个程序，上述参数化模型检查问题的通用片段的u演算，使它总是终止，但可能会给假阴性。我们还推出了参数化的模型检测问题的泛析取自由片段的u演算是可判定的。对于具有阵列的数据独立系统的模型检验的实际动机包括存储器和高速缓存系统的验证，其中X是存储器地址的类型，并且Y是可存储值的类型。作为一个例子，我们验证了一组不可靠的存储器的容错存储器接口。
英文摘要：
A system is data-independent with respect to a data type X iff the operations it can perform on values of type X are restricted to just equality testing. The system may also store, input and output values of type X. We study model checking of systems which are data-independent with respect to two distinct type variables X and Y, and may in addition use arrays with indices from X and values from Y . Our main interest is the following parameterised model-checking problem: whether a given program satisfies a given temporal-logic formula for all non-empty nite instances of X and Y . Initially, we consider instead the abstraction where X and Y are infinite and where partial functions with finite domains are used to model arrays. Using a translation to data-independent systems without arrays, we show that the u-calculus model-checking problem is decidable for these systems. From this result, we can deduce properties of all systems with finite instances of X and Y . We show that there is a procedure for the above parameterised model-checking problem of the universal fragment of the u-calculus, such that it always terminates but may give false negatives. We also deduce that the parameterised model-checking problem of the universal disjunction-free fragment of the u-calculus is decidable. Practical motivations for model checking data-independent systems with arrays include verification of memory and cache systems, where X is the type of memory addresses, and Y the type of storable values. As an example we verify a fault-tolerant memory interface over a set of unreliable memories.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
