学位论文 > 优秀研究生学位论文题录展示

基于概率模型检测的生存性分析与验证方法研究

作　者: 张兵
导　师: 周清雷
学　校: 郑州大学
专　业: 计算机软件与理论
关键词: 概率模型检测生存性分析补偿约束 PRISM检测器 DTMC模型
分类号: TP274
类　型: 硕士论文
年　份: 2012年
下　载: 121次
引　用: 0次
阅　读: 论文下载

内容摘要

模型检测作为一种重要的形式化验证技术,具有可靠、高效的优点,能够实现自动验证,获得了越来越多的关注,并在硬件电路、通信协议、控制系统、安全认证协议等方面的分析与验证中取得了巨大的成功。BDDs、符号化模型检测等优化技术的出现,很大程度上缓解了状态爆炸问题,使模型检测工业化应用成为可能。生存性作为软硬件系统抵御灾难、自我修复能力的描述,成为网络研究的一个热点。生存性的准确定义尚不明确,其定义及分析方法的研究是生存性研究的主要方向。论文将模型检测技术应用于生存性分析,深入研究了形式化分析生存性的方法。完成的主要工作如下：1、阐述了模型检测的框架和概率模型检测的内容,详细介绍了基于DTMC、 CTMC、 PTA模型的三类不同的概率模型检测方法,深入分析了这些概率模型检测的特点、表述的能力和实现的难易程度。2、在生存性及概率模型检测的基础上,提出了验证生存性的模型检测方法。首先给出适用于模型检测的生存性定义,以及采用模型检测验证生存性的方法；然后采用PRISM,对电话接入网建模并验证其生存性。通过与数值计算的结果对比分析,证明了形式化方法分析生存性的正确性。3、针对考虑时延、能耗约束的随机系统验证问题,提出了带有补偿约束的概率模型检测方法。首先构造带补偿约束的DTMC模型,并转化成等价的权重图。以满足约束且概率最大为原则,将反例生成转换成权重图上多约束最短路径问题；其次扩展LTL-x逻辑,使其包含状态公式与路径补偿公式,修改后的概率模型检测具备了描述与验证补偿约束的能力。带补偿的概率模型转换成权重图的方法,保持模型满足约束状态及相应路径的不变,权重图上多约束最短路径问题可解性保证了带补偿约束模型检测的可行性。最后对本文的工作进行了总结,指出论文存在的不足,并对进一步的工作进行展望。

全文目录

摘要  4-5
Abstract  5-7
目录  7-9
1 绪论  9-13
  1.1 研究背景  9-10
  1.2 研究现状  10-11
  1.3 研究内容  11-12
  1.4 论文组织结构  12-13
2 模型检测技术  13-18
  2.1 模型检测的定义  13-15
  2.2 模型检测的特点  15
  2.3 模型检测的难题及优化技术  15-18
3 概率模型检测  18-25
  3.1 离散马尔科夫链模型  18-20
  3.2 连续马尔科夫模型  20-22
  3.3 概率时间自动机模型  22-24
  3.4 本章小结  24-25
4 基于模型检测的生存性分析  25-34
  4.1 生存性定义及验证方法  25-26
  4.2 电话接入网的生存性分析  26-29
  4.3 实验分析  29-32
    4.3.1 PRISM简介  29-30
    4.3.2 模型与生存性描述  30-31
    4.3.3 实验结果  31-32
  4.4 本章小结  32-34
5 带补偿约束的概率模型检测  34-44
  5.1 带补偿约束的DTMC  34-35
  5.2 描述补偿的LTL_x逻辑  35-37
  5.3 反例及生成方法  37-42
    5.3.1 修改DTMC  38
    5.3.2 DTMC转换成权重图  38-40
    5.3.3 最小反例生成算法  40-42
  5.5 本章小结  42-44
6 总结与展望  44-46
  6.1 论文总结  44-45
  6.2 论文的不足和展望  45-46
参考文献  46-50
致谢  50-51
个人简历及发表论文情况  51
  个人简历  51
  硕士期间发表论文  51

基于概率模型检测的生存性分析与验证方法研究

内容摘要

全文目录

相似论文