A Generalised Sweep-Line Method for Safety Properties
A Generalised Sweep-Line Method for Safety Properties
复制标题
安全特性的广义扫描线法
DOI：
10.1007/3-540-45614-7_31
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
T. Mailund
中科院分区：
文献类型：
--
作者：
L. Kristensen;T. Mailund
最近开发的扫描线方法利用许多并发系统中存在的进展来探索系统的完整状态空间，同时一次仅将状态空间的一小部分存储在内存中。扫线方法的缺点是它依赖于单调且全局的进展概念。这使得该方法无法用于许多反应式系统。在本文中，我们推广了扫线方法，使其可用于验证表现出局部进展的反应系统的安全特性。基本思想是放宽单调的进步概念，并认识到这可能导致状态空间探索不终止的情况。广义扫线方法探索系统的所有可达状态，但可能会多次探索一个状态。我们在两个案例研究中展示了广义扫描线方法的实际应用，证明与使用普通全状态空间相比，峰值内存使用量通常减少到 10%。
The recently developed sweep-line method exploits progress present in many concurrent systems to explore the full state space of the system while storing only small fragments of the state space in memory at a time. A disadvantage of the sweep-line method is that it relies on a monotone and global notion of progress. This prevents the method from being used for many reactive systems. In this paper we generalise the sweep-line method such that it can be used for verifying safety properties of reactive systems exhibiting local progress. The basic idea is to relax the monotone notion of progress and to recognise the situations where this could cause the state space exploration not to terminate. The generalised sweep-line method explores all reachable states of the system, but may explore a state several times. We demonstrate the practical application of the generalised sweep-line method on two case studies demonstrating a reduction in peak memory usage to typically 10 % compared to the use of ordinary full state spaces.