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

模型检测在模型诊断领域中的应用

作　者: 廉智超
导　师: 欧阳丹彤
学　校: 吉林大学
专　业: 计算机软件与理论
关键词: 模型检测时态逻辑有序二元决策图基于模型诊断可诊断性
分类号: TP277
类　型: 硕士论文
年　份: 2007年
下　载: 180次
引　用: 0次
阅　读: 论文下载

内容摘要

模型检测技术从诞生之日起已经走过了二十五年的历程,事实证明,这种技术是目前最成功的形式化验证技术之一,本文主要围绕模型检测在模型诊断领域中的应用展开研究,主要内容有:1.详细研究了模型检测在动态模型可诊断性判定中的应用,并与传统的判定方法进行对比,对它的不足之处进行了修正,最后给出了在特殊情况下节省时间的方法。2.详细研究了模型检测在静态模型可诊断性判定中的应用,将这种方法应用在开源诊断系统Livingstone的可诊断性判定中,并结合模型特点针对模型检测器给出相关检测优化方案。3.为了满足诊断的实时性要求,将模型检测应用到了动态系统的模型诊断中,提出了一种基于模型检测的实时诊断方法,这种方法的优势在于将状态空间符号化,通过高效模型检测算法来进行诊断,既节省空间,又能够提高诊断效率。最后对这一方法进行了系统实现,通过实验验证了这种方法的可行性。

全文目录

提要  4-7
第一章引言  7-10
  1.1 研究背景  7-8
  1.2 与基于模型诊断结合的研究意义  8-9
  1.3 本文主要工作  9-10
第二章模型检测知识  10-21
  2.1 KRIPKE 结构  10-11
  2.2 时态逻辑  11-15
  2.3 模型检测的过程  15-16
  2.4 符号模型检测理论  16-20
  2.5 有界模型检测简介  20-21
第三章基于模型检测的动态模型可诊断性研究  21-36
  3.1 离散事件系统简介  21
  3.2 离散事件系统故障诊断过程  21-22
  3.3 基本概念  22-23
  3.4 LTL 公式与BUCHI 自动机的关系  23-24
  3.5 LTL 故障说明的离散事件诊断方法  24-32
  3.6 多故障说明的扩展  32-33
  3.7 预先可诊断性相关讨论  33-35
  3.8 小结  35-36
第四章基于模型检测的静态模型可诊断性研究  36-49
  4.1 可诊断性问题介绍  36-37
  4.2 可诊断性问题的判定方法  37-39
  4.3 LIVINGSTONE 系统简介  39-40
  4.4 LIVINGSTONE 到NUSMV 的模型转换  40-42
  4.5 双模型构建方法  42
  4.6 反例路径向LIVINGSTONE 系统模型的转化  42-43
  4.7 优化策略  43-48
  4.8 小结  48-49
第五章基于模型检测技术的实时状态诊断方法  49-60
  5.1 理论框架  50-54
  5.2 可诊断性  54-56
  5.3 实时诊断方法  56-58
  5.4 小结  58-60
第六章系统实现与实验分析  60-66
  6.1 系统建模部分  60-61
  6.2 CTL 模型检测部分  61-64
  6.3 反例路径生成方法  64
  6.4 实验测试  64-66
第七章总结与展望  66-68
  7.1 总结  66
  7.2 展望  66-68
作者在读期间发表的论文  68-69
参考文献  69-72
摘要  72-75
ABSTRACT  75-78
致谢  78-79
导师及作者简介  79

相似论文

羊种布鲁氏菌16M优势蛋白抗原的鉴定,S852.61
基于BMC的Web服务失配检测方法研究,TP311.52
基于四方的安全电子商务支付协议研究,TP393.08
132例女性疑难腹水的诊断分析与研究,R442.5
安全协议自动化分析系统的设计与实现,TP393.08
Web服务事务协调协议WS-TX的形式化分析与验证,TP393.09
基于UPPAAL的电子商务协议安全性分析,TP393.08
基于模型检测方法的可信软件验证技术研究,TP311.52
面向环境演算系统的模型检测算法的研究,TP274
网络安全协议的模型检测分析及验证系统,TP393.08
基于程序语义的静态恶意代码检测系统的研究与实现,TP393.08
可重配置硬件系统调度算法的模拟与分析,TN791
MBD在配电网故障诊断中的应用研究,TM711
白三烯D4支气管激发试验方法学的建立及其系列临床研究,R562.25
时间感知Web服务交互适配技术研究,TP393.09
基于XYZ/ADL的Web服务组合验证研究,TP393.09
基于Color Petri Nets的HMIPv6协议形式化验证研究,TN929.5
江西省高校信息化评估研究,G640
C.TEST阅读理解测验的诊断性评价研究,H195
汉语作为第二语言学习者量词掌握模式诊断研究,H195
汉语作为第二语言的阅读理解诊断性成绩测试研究,H195