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