无穷状态系统可覆盖性分析算法

摘要：

针对良序结构迁移系统可覆盖性分析计算成本高的问题, 提出一种运用有限状态模型检验技术解决无穷状态系统可覆盖性问题的算法. 首先将良序结构迁移系统划分为不同权值限定下的一系列有限状态机模型; 然后采用最新的模型检验技术增量式地计算不同权值下模型的可达状态空间上逼近, 得到可覆盖的反例路径或证明该系统不可覆盖. 实验结果表明, 该算法在同等计算时间限制下能够解决更多的测试样例; 在1 GB 内存限制下, 可以解决97.2%的测试样例, 超过同类算法的2倍.

关键词：良序结构迁移系统、无穷状态系统、可覆盖性分析、Petri网、IC3

所属期刊栏目：30

分类号：TP302(计算技术、计算机技术)

资助基金：国家自然科学基金重点项目61133007

在线出版日期：2018-06-20（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：1145-1151