关于不带重置的数组数据无关系统的模型检查
摘要：具有类型X的数据类型的系统与数据无关，当且仅当它可以对X类型的值执行的操作仅限于相等性测试。该系统还可以存储，输入和输出X类型的值。我们研究了与两个不同类型变量X和Y无关的系统的模型检查，并且还可以使用来自X和Y的数组索引和值。我们主要关注以下参数化模型检查问题：对于所有非空有限的X和Y的实例，给定的程序是否满足给定的时间逻辑公式。最初，我们考虑X和Y无限的抽象，使用具有有限定义域的偏函数来对数组进行建模。通过将其转换为不带数组的数据无关系统，我们证明了对这些系统的u-算法模型检查问题是可决的。从此结果，我们可以推断出对于所有有限的X和Y实例的系统的属性。我们证明了对于u-算法通用片段的上述参数化模型检查问题存在一个过程，它总是终止但可能给出错误的否定答案。我们还推断出u-算法通用无析取片段的参数化模型检查问题是可决的。对于具有数组的数据无关系统进行模型检查的实际动机包括验证内存和高速缓存系统，其中X是内存地址的类型，而Y是可存储值的类型。作为一个例子，我们验证了一个容错内存接口在一组不可靠的内存中。
作者：R.S. Lazic, T.C. Newcomb, A.W. Roscoe
论文ID：cs/0405103
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23