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

A deadlock model detection algorithm with heuristic factors

作　　者：王焱 吴涛[1] 杨斐 WANG Yan;WU Tao;YANG Fei(School of Computer Science,Chengdu University of Information Technology,Chengdu 610225,China;Key Laboratory of Nuclear Reactor System Design Technology,Nuclear Power Institute of China,Chengdu 610041,China)

机构地区：[1]成都信息工程大学计算机学院,成都610225 [2]中国核动力研究设计院核反应堆系统设计技术重点实验室,成都610041

出　　处：《重庆理工大学学报（自然科学）》2022年第12期305-312,共8页Journal of Chongqing University of Technology：Natural Science

基　　金：四川省科技计划项目(2021YFQ0056,2021YFS0396,2019ZDZX0001)。

摘　　要：提出了一种基于差分进化算法的模型检测算法,用以解决模型检测中的死锁检测问题。模型检测方法通过抽象出一个系统的模型和定义关于该系统的具体规范,模型检测器就可以自动验证系统是否满足规范。由于一般的显式模型检测器是采用确定性算法来完成检测的(如深度优先搜索),因此在对状态空间较大的系统进行检测时,模型检测的效率较低,甚至不能完成检测。为了缓解这种问题,提出了一种基于差分进化算法的启发式模型检测算法。同时基于原有算法框架扩展了基于路径的编码、模拟退火、关键参数自适应等操作用于提高算法表现。结果表明,该算法可以在较少的时间内找到含有死锁状态的反例路径,并且与确定性算法和2种不确定性算法(粒子群算法,遗传算法)比较,在状态搜索方面与生成反例长度方面均有更好的表现。In this paper, a model detection algorithm based on differential evolution algorithm is proposed to solve the problem of deadlock detection in model detection. By abstracting a systematic model and defining detailed specifications of the system, the model detector can automatically verify whether the system meets the specifications. Because a general explicit model detector uses deterministic algorithms to complete the detection such as depth-first search, the efficiency of model detection is low, or it even fails to complete the detection when detecting a system with large state space. To alleviate this problem, a heuristic model detection algorithm based on differential evolution algorithm is proposed. At the same time, based on the original algorithm framework, an extension of path-based coding, simulated annealing, key parameter self-adaptation and other operations is done to improve the performance of the algorithm. The results show that the algorithm can find the counterexample path with a deadlock state in less time, and is superior to many other algorithms in terms of state search and length of counterexample generation, including deterministic algorithm BFS, two indeterministic algorithms, particle swarm algorithm(PSO), and genetic algorithm(GE).

关 键 词：模型检测 差分进化算法 死锁检测 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]