首页|带有启发式因子的死锁模型检测算法

带有启发式因子的死锁模型检测算法

A deadlock model detection algorithm with heuristic factors

扫码查看
提出了一种基于差分进化算法的模型检测算法,用以解决模型检测中的死锁检测问题.模型检测方法通过抽象出一个系统的模型和定义关于该系统的具体规范,模型检测器就可以自动验证系统是否满足规范.由于一般的显式模型检测器是采用确定性算法来完成检测的(如深度优先搜索),因此在对状态空间较大的系统进行检测时,模型检测的效率较低,甚至不能完成检测.为了缓解这种问题,提出了一种基于差分进化算法的启发式模型检测算法.同时基于原有算法框架扩展了基于路径的编码、模拟退火、关键参数自适应等操作用于提高算法表现.结果表明,该算法可以在较少的时间内找到含有死锁状态的反例路径,并且与确定性算法和2种不确定性算法(粒子群算法,遗传算法)比较,在状态搜索方面与生成反例长度方面均有更好的表现.

王焱、吴涛、杨斐

展开 >

成都信息工程大学 计算机学院, 成都 610225

中国核动力研究设计院 核反应堆系统设计技术重点实验室, 成都 610041

模型检测 差分进化算法 死锁检测

四川省科技计划四川省科技计划四川省科技计划

2021YFQ00562021YFS03962019ZDZX0001

2022

重庆理工大学学报
重庆理工大学

重庆理工大学学报

CSTPCD北大核心
影响因子:0.567
ISSN:1674-8425
年,卷(期):2022.36(12)
  • 4