针对良序结构迁移系统可覆盖性分析计算成本高的问题, 提出一种运用有限状态模型检验技术解决无穷状态系统可覆盖性问题的算法. 首先将良序结构迁移系统划分为不同权值限定下的一系列有限状态机模型; 然后采用最新的模型检验技术增量式地计算不同权值下模型的可达状态空间上逼近, 得到可覆盖的反例路径或证明该系统不可覆盖. 实验结果表明, 该算法在同等计算时间限制下能够解决更多的测试样例; 在1 GB 内存限制下, 可以解决97.2%的测试样例, 超过同类算法的2倍.%We propose a novel algorithm for coverability analysis in a broad class of infinite-state systems named well-structured transition systems by using finite-state model checking techniques. Firstly, the well-structured transition system is divided into a series of finite-state machines with different weights. Then, the state-of-the-art model checking algorithm is used to compute the over-approximation of the reachability for the finite state machines, incrementally. Finally, the algorithm produces a coverable counterexample path or proves the system is uncoverable. The results show that the algorithm can solve more instances under the same time limit. 97.2% instances are solved within 1 GB memory, which is more than two times of the compared algorithms.
展开▼
