State-space caching revisited
State-space caching revisited
复制标题
重新审视状态空间缓存
DOI：
10.1007/bf01384077
复制
发表时间：
1992
影响因子：
0.8
通讯作者：
Didier Pirottin
中科院分区：
文献类型：
--
作者：
Patrice Godefroid;G. Holzmann;Didier Pirottin
状态空间缓存是一种有限状态并发系统的验证技术。它对被检查系统的状态空间进行详尽的探索，同时只存储一个执行序列的所有状态以及可用内存允许的尽可能多的其他先前访问过的状态。到目前为止，这种技术还没有什么实际意义：它只允许将内存使用减少2到3倍，否则就会出现不可接受的运行时开销激增。运行时需求的激增是由于对状态空间的未存储部分进行冗余的多次探索。实际上，在搜索过程中，几乎并发系统状态空间中的所有状态通常都要到达几次。在本文中，我们提出了一种方法来解决这种禁止状态匹配的主要原因：探索系统并发执行的所有可能的交错，这些交错都导致相同的状态。然后，我们证明，在许多情况下，使用该方法，大多数可达状态在状态空间探索过程中只被访问一次。这使得不需要存储已经访问过的大部分状态，而不会导致对部分状态空间进行过多的冗余探索，因此使状态空间缓存成为一种更有吸引力的验证方法。例如，我们能够完全探索包含250,000个状态的状态空间，同时存储不超过500个状态，并且运行时需求仅增加了三倍。
State-space caching is a verification technique for finite-state concurrent systems. It performs an exhaustive exploration of the state space of the system being checked while storing only all states of just one execution sequence plus as many other previously visited states as available memory allows. So far, this technique has been of little practical significance: it allows one to reduce memory usage by only twoo to three times, before an unacceptable blow-up of the run-time overhead sets in. The explosion of the run-time requirements is due to redundant multiple explorations of unstored parts of the state space. Indeed, almost all states in the state space of concurrent systems are typically reached several times during the search.In this paper, we present a method to tackle the main cause of this prohibitive state matching: the exploration of all possible interleavings of concurrent executions of the system which all lead to the same state. Then, we show that, in many cases, with this method, most reachable states are visited only once during state-space exploration. This enables one not to store most of the states that have already been visited without incurring too much redundant explorations of parts of the state space, and makes therefore state-space caching a much more attractive verification method. As an example, we were able to competely explore a state space of 250,000 states while storing simultaneously no more than 500 states and with only a three-fold increas of the run-time requirements.