传播最大和最新接受前驱的On-the-Fly并行空性检测

摘要：

针对一种结合最大接受前驱的on-the-fly并行空性检测方法,在接受环最大接受前驱处于环外的情境,无法通过传播接受前驱以on-the-fly方式识别接受环的问题,提出一种传播最大和最新接受前驱的on-the-fly并行空性检测方法.在首次遍历积自动机时,它采用最大接受前驱和最新接受前驱的双值传播模式,最大接受前驱仍保留原方法的传播特征,引入的最新接受前驱追踪并行空性检测的局部遍历特征,使其在原方法传播接受前驱识别失效时仍能on-the-fly识别接受环.理论证明了该算法的正确性,对比实验验证了该算法提前终止率更高,时空成本更低,on-the-fly优势更强.在软件模型检测领域,该方法为并行空性检测进一步控制状态空间爆炸,提供了一种有效途径.

关键词：软件模型检测、并行空性检测、Büchi自动机、on-the-fly方法

所属期刊栏目：36

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

资助基金：国家自然科学基金项目61370083,61073043,61073041;高等学校博士学科点专项科研基金项目20112304110011,20122304110012;哈尔滨市科技创新人才研究专项资金项目2011RFXXG015

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

页数：共6页

页码：1203-1208