Computing Reachable Control States of Systems Modeled with Uninterpreted Functions and Infinite Memory
Computing Reachable Control States of Systems Modeled with Uninterpreted Functions and Infinite Memory
复制标题
计算使用未解释函数和无限内存建模的系统的可达控制状态
DOI：
10.1007/bfb0028750
复制
发表时间：
1998
期刊：
影响因子：
--
通讯作者：
R. Brayton
中科院分区：
文献类型：
--
作者：
Adrian J. Isles;R. Hojati;R. Brayton
我们提出了一种方法，自动计算的控制状态集可达系统建模与未解释的功能，谓词和无限的内存。一般来说，以这种方式建模的系统的抽象状态空间是无限的，并且基于精确状态枚举的过程可能不会终止。使用组合顺序（ICS）并发模型[HB95]作为我们的基础形式主义，我们展示了如何“在飞行中”状态约简技术，保持控制不变性，可用于显着加速可达性计算这样的抽象硬件表示，在某些情况下，折叠无限状态空间有限的。本文提出的方法是自动的，如果它终止，将产生的抽象硬件模型的可达控制状态的确切集合。我们的技术已实现在ICS状态可达性工具和实验结果给出了几个例子。
We present an approach for automatically computing the set of control states reachable in systems modeled with uninterpreted functions, predicates and infinite memory. In general, the abstract state spaces of systems modeled in this fashion are infinite and exact state enumeration based procedures may not terminate. Using the Integer Combinational Sequential (ICS) concurrency model [HB95] as our underlying formalism, we show how ‘on-the-fly’ state reduction techniques, which preserve control invariance properties, can be used to significantly speed-up reachability computations on such abstract hardware representations, collapsing infinite state spaces to finite ones in some cases. The approach presented in this paper is automatic and if it terminates, will produce the exact set of reachable control states of abstract hardware models. Our techniques have been implemented in an ICS state reachability tool and experimental results are given on several examples.