基于模型检测的可诊断性的形式化检验研究-自动化技术-论文之家

您现在的位置：硕士论文 >> 电子论文 >> 自动化 >> 自动化技术 >> 正文

基于模型检测的可诊断性的形式化检验研究

作者：黄丫 Publish: 2006-8-4 Hits:-

【中文题名】

基于模型检测的可诊断性的形式化检验研究

【英文题名】

Research on Formal Verification of Diagnosability Via Model-Checking

【学科专业】

计算机软件与理论

【论文级别】

硕士论文

【投稿时间】

2006-8-4

【中关键词】

模型检测,时序逻辑,可诊断性,临界对,耦合孪生模型,

【英关键词】

【分类导航】

工业技术>自动化技术、计算机技术>自动化技术及设备>自动化系统>数据处理、数据处理系统>数据收集和处理系统

【论文摘要】

模型检测是近二十几年来最成功的自动检验技术之一,它是关于系统属性验证的算法和方法。它通常采用状态空间搜索的方法来检测一个给定的计算模型是否满足某个用时序逻辑公式表示的特定属性。它是一个自动检验有限状态并发系统的技术。和基于模拟、测试和演绎推理问题的传统方法相比较,有着许多的优点,也已经成功地实践于检验复杂的时序电路设计和通讯协议。本文首先介绍了模型检测的一些基本概念和理论,然后介绍了与其密切相关的、在检验中用于描述系统属性的时序逻辑,及实现模型检测问题的方法,在基于上述关于概念、理论的基础上,研究了诊断系统可诊断性的检验方法,说明了一个给定设备的诊断条件被破坏时当且仅当有临界对的出现,并定义了设备的耦合孪生模型,说明如何用它来寻找临界对,最后使用模型检测框架来构造这个问题,把耦合孪生模型化简为模型检测问题。

【论文题纲】

第一章引言	7-9
1.1 研究背景	7
1.2 本文主要内容	7-9
第二章模型检测	9-20
2.1 与其它形式检验方法的比较	9-10
2.2 模型检测方法的步骤	10-11
2.3 Kripke 结构	11
2.4 系统建模	11-20
2.4.1 一阶逻辑表示	12-14
2.4.2 变迁粒度	14-15
2.4.3 并发系统建模	15-20
第三章时序逻辑的概述	20-29
3.1 CTL*计算树逻辑	20-23
3.1.1 基本概念	21-22
3.1.2 关于Kripke结构的CTL*语义	22-23
3.2 CTL 和LTL	23-26
3.2.1 CTL	24-25
3.2.2 LTL	25-26
3.3 CTL*，CTL 和LTL 的关系	26-27
3.4 合理性约束	27-29
第四章模型检测问题的实现	29-42
4.1 CTL 模型检测	29-35
4.1.1 一般实现方法	29-34
4.1.2 基于合理性约束的实现	34-35
4.2 LTL 模型检测	35-42
第五章可诊断性的形式化检验	42-53
5.1 简介	42
5.2 基本假设	42-45
5.3 可诊断性	45-47
5.4 耦合孪生设备	47-50
5.5 基于模型检测的可诊断性	50-52
5.5.1 可诊断性的Kripke 结构	50-51
5.5.2 符号表示法	51
5.5.3 时序逻辑的应用	51-52
5.6 结论	52-53
第六章总结与展望	53-54
参考文献	54-56
摘要	56-59
Abstract	59-62
致谢	62-63
导师及作者简介	63

【DOI】

LunWen.ID:2.2008.379474



付费论文：有参考文献 300元

1、注册会员 2、购买本文 3、下载文章
注:此文为收费论文，需付费购买。每页大约1000字。

代写论文流程

载入中…

Web lunwenjia


热门搜索：模型检测论文时序逻辑可诊断性临界对耦合孪生模型

自动化技术最新论文

自动化技术热门论文