基于启发式遗传算法生成随机模型检验的反例

论文摘要

模型检验的主要优势之一是它能够在模型违反给定时态逻辑的情况下自动生成反例。反例提供了用于系统调试时的基本诊断信息,调试者可以根据反例,分析系统错误产生的原因,进而对系统进行修正,反例在调试复杂系统时可以提供很大的帮助。在随机模型检验中生成反例时使用精确算法通常会消耗太多的时间和内存,并且有时无法找到反例。更糟糕的是,在随机模型检验中生成smallest反例已被证明是NP完全问题,并且不太可能有效逼近。尽管有一些启发式方法应用于反例的生成,但通常很难确定启发式函数,而启发式函数的确定对反例的生成至关重要。本文中,我们提出一种基于启发式遗传算法的方法生成随机模型检验中的反例。定义诊断子图(diagnostic subgraph)表示反例,并通过启发式方法扩展遗传算法(Heuristic Genetic Algorithm,HGA)生成反例。该方法采用间接路径编码方案以扩展状态空间的搜索范围,并采用启发式方式生成更有效的路径。具体内容如下:(1)将DTMC和MDP转换成对应的状态迁移图,HGA直接在状态迁移图上进行搜索;(2)在实现启发式方法扩展遗传算法的过程中,使用了间接路径编码方案和启发式算子,并且设计了合适的适应度函数;(3)通过HGA生成DTMC中违反可达性质的反例,当诊断子图的概率超出给定的概率阈值,该诊断子图即为反例;(4)通过HGA生成MDP中违反可达性质的反例,为了让组成反例的诊断路径在调度程度下均为有效路径,将诊断路径的集合转换为AND/OR树,进而生成反例。最后,通过实例研究说明本文提出的算法具有良好的可行性和有效性。实验结果表明,在随机模型检验中,HGA算法优于现有的反例生成算法。

论文目录

• 摘要
• ABSTRACT
• 第一章 绪论
•   1.1 研究意义
•   1.2 国内外研究现状
•     1.2.1 模型检验中的反例的生成
•     1.2.2 随机模型检验中的反例生成
•     1.2.3 遗传算法的发展
•   1.3 研究目标与内容
•   1.4 本文创新
•   1.5 论文组织结构
• 第二章 随机模型检验及反例
•   2.1 马尔科夫链
•   2.2 马尔科夫决策过程
•   2.3 概率度量
•     2.3.1 路径和概率度量
•     2.3.2 调度程度和概率度量
•   2.4 概率计算树逻辑
•   2.5 可达性
•     2.5.1 DTMC可达性
•     2.5.2 MDP可达性
•   2.6 反例的概念
•     2.6.1 DTMC中的反例
•     2.6.2 MDP中的反例
•   2.7 本章小结
• 第三章 遗传算法
•   3.1 基本过程
•   3.2 遗传算子
•   3.3 遗传算法的特点
•   3.4 本章小结
• 第四章 启发式遗传算法生成反例
•   4.1 启发式遗传算法
•     4.1.1 编码
•     4.1.2 适应度函数
•     4.1.3 交叉算子
•     4.1.4 变异算子
•   4.2 反例的生成
•     4.2.1 状态迁移图
•     4.2.2 DTMC中的反例生成
•     4.2.3 MDP中的反例生成
•   4.3 本章小结
• 第五章 实例研究
•   5.1 动态电源管理
•   5.2 同步领导人选举协议
•   5.3 人群协议
•   5.4 IPv4 Zeroconf协议
•   5.5 有界重传协议
•   5.6 本章小结
• 第六章 总结与展望
•   6.1 本文工作总结
•   6.2 研究展望
• 参考文献
• 研究生期间的科研成果
• 致谢

文章来源

类型: 硕士论文

作者: 郑婷婷

导师: 刘阳

关键词: 反例,随机模型检验,启发式,遗传算法

来源: 南京财经大学

年度: 2019

分类: 基础科学,信息科技

专业: 数学,计算机软件及计算机应用,自动化技术

单位: 南京财经大学

分类号: TP311.5;O211.6;TP18

DOI: 10.27705/d.cnki.gnjcj.2019.000336

总页数: 66

文件大小: 2798K

下载量: 13