Verification of Timed Systems Using POSETs
Verification of Timed Systems Using POSETs
复制标题
使用 POSET 验证定时系统
DOI：
10.1007/bfb0028762
复制
发表时间：
1998
期刊：
影响因子：
--
通讯作者：
C. Myers
中科院分区：
文献类型：
--
作者：
W. Belluomini;C. Myers
本文提出了一种新的算法，有效地验证时间系统。新算法使用几何区域表示定时信息，并通过考虑事件的偏序集而不是线性序列来探索定时状态空间。这种方法通过显著降低系统中定时状态与非定时状态的比率，避免了高度并发系统中典型的定时状态爆炸。一般类的定时系统，其中包括事件和水平的因果关系可以指定和验证。该算法被应用到最近的几个定时基准测试显示在运行时间和内存使用的数量级的改善。
This paper presents a new algorithm for efficiently verifying timed systems. The new algorithm represents timing information using geometric regions and explores the timed state space by considering partially ordered sets of events rather than linear sequences. This approach avoids the explosion of timed states typical of highly concurrent systems by dramatically reducing the ratio of timed states to untimed states in a system. A general class of timed systems which include both event and level causality can be specified and verified. This algorithm is applied to several recent timed benchmarks showing orders of magnitude improvement in runtime and memory usage.