构件系统模型检测方法研究

发布时间：2017-10-16 15:35

  本文关键词：构件系统模型检测方法研究

  更多相关文章： 构件系统 模型检测 抽象方法

【摘要】：构件系统被广泛应用于许多工业领域,全面的分析其行为和正确性具有现实需求和意义。现已有对该系统交互及随机行为正确性进行验证的符号化、组合和统计模型检测方法。由于构件系统中变量较多,容易引起验证的状态空间爆炸问题;而使用抽象技术时,验证是不完备的。针对以上问题,围绕对构件系统中变量的处理,本文提出了一些模型检测方法,并将它们用于实际案例的的验证。本文的主要贡献如下:?本文提出了基于变量划分的符号化模型检测方法。该方法对分离迁移表达式中的变量集合进行划分,将其分为值变化和值不变的两个子集。使用该方法进行构件系统符号化模型检测时,只需要对迁移上值变化的变量进行处理,有效地减少了时间和内存开销。?本文针对组合抽象构件系统不变式验证的不完备问题,提出了不变式增强和状态划分两种精化方法。不变式增强方法主要用于去除系统伪反例,并生成增强不变式精化原系统不变式;状态划分方法主要利用反例对抽象状态进行划分,生成新状态对抽象系统进行精化。将上述两种精化方法融入到组合抽象方法中,本文提出了构件系统抽象精化组合模型检测算法,并证明了该算法的完备性和有效性。?为了对随机构件模型行为属性进行概率分析和检测,本文设计并实现了模型翻译和基于模块的系统组合方法,其保留了原模型的概率信息和构件系统的组合特性。本文使用概率变量分布离散化方法对复杂模型进行抽象,并对抽象模型的概率模型检测和原模型的统计模型检测方法进行比较和分析。?为了分析带权随机构件系统期望的性质,针对已有i LTL方法只能对非周期Markov模型进行验证的问题,本文提出了对周期Markov模型的概率质量函数(pmf)序列的时序属性进行基于可行解的模型检测方法——ip LTL。上述验证方法使用了抽象技术,将pmf作为模型状态。当待验证属性不成立时,该方法将给出反例,即模型的初始pmf。从该初始pmf出发,可以对违反属性的系统运行进行分析。
【关键词】：构件系统 模型检测 抽象方法
【学位授予单位】：清华大学
【学位级别】：博士
【学位授予年份】：2015
【分类号】：O213
【目录】：

• 摘要3-4
• Abstract4-9
• 第1章 绪论9-21
• 1.1 研究对象9-11
• 1.2 研究目标11-13
• 1.3 相关研究工作13-18
• 1.3.1 符号化模型检测13-14
• 1.3.2 组合模型检测14-16
• 1.3.3 统计模型检测16-17
• 1.3.4 概率模型检测17
• 1.3.5 模型检测工具17-18
• 1.4 研究思路18-20
• 1.5 论文贡献20
• 1.6 论文结构20-21
• 第2章 构件系统21-30
• 2.1 引言21-22
• 2.2 构件系统22-24
• 2.3 随机构件系统24-27
• 2.4 带权随机构件系统27-29
• 2.5 本章小结29-30
• 第3章 构件系统符号化模型检测30-41
• 3.1 引言30-31
• 3.2 符号化模型检测31-33
• 3.2.1 符号化模型检测31-32
• 3.2.2 分离迁移表达式方法32
• 3.2.3 变量划分方法32-33
• 3.3 构件系统符号化模型33-34
• 3.4 构件系统符号化模型检测34-36
• 3.4.1 构件系统变量划分34-35
• 3.4.2 变量划分符号化算法35-36
• 3.5 案例及实验结果分析36-40
• 3.6 本章小结40-41
• 第4章 构件系统抽象精化组合模型检测41-64
• 4.1 引言41-43
• 4.2 组合抽象构件系统模型检测43-48
• 4.2.1 组合验证规则43-47
• 4.2.2 组合验证的不完备性问题分析47-48
• 4.3 精化方法48-52
• 4.3.1 不变式增强48-49
• 4.3.2 状态划分49-52
• 4.4 构件系统验证框架52-56
• 4.5 案例分析56-62
• 4.5.1 车门控制系统56-57
• 4.5.2 温度控制系统57-62
• 4.6 本章小结62-64
• 第5章 随机构件系统概率分析和检测64-79
• 5.1 引言64-65
• 5.2 PRISM建模语言65-66
• 5.3 随机构件系统模型翻译66-69
• 5.4 构件系统随机行为分析69-77
• 5.4.1 时钟同步协议案例70-72
• 5.4.2 统计模型检测72-73
• 5.4.3 模型抽象73-74
• 5.4.4 概率模型检测74-75
• 5.4.5 MPEG2播放器案例75-77
• 5.5 本章小结77-79
• 第6章 基于可行解的随机构件系统模型检测79-96
• 6.1 引言79-80
• 6.2 随机构件系统语义分析80-81
• 6.3 iLTL模型检测81-84
• 6.4 ipLTL模型检测84-93
• 6.4.1 (k, d)-Markov模型及其收敛性分析84-88
• 6.4.2 ip LTL的语法和语义88-89
• 6.4.3 ip LTL模型检测89-93
• 6.5 案例分析93-94
• 6.6 本章小结94-96
• 第7章 结束语96-98
• 7.1 工作总结96-97
• 7.2 研究展望97-98
• 参考文献98-105
• 致谢105-107
• 个人简历、在学期间发表的学术论文与研究成果107

【相似文献】

中国期刊全文数据库 前1条

1 黎云祥，刘玉成，，钟章成;植物种群生态学中的构件理论[J];生态学杂志;1995年06期

中国重要报纸全文数据库 前1条

1 卢捍华 刘建星;NGOSS：运营支撑系统的新框架[N];通信产业报;2003年

中国博士学位论文全文数据库 前2条

1 张连怡;构件系统模型检测方法研究[D];清华大学;2015年

2 黄杰;分布构件系统故障诊断技术研究[D];国防科学技术大学;2005年

中国硕士学位论文全文数据库 前6条

1 苏萍;面向动态更新的构件依赖自动管理技术研究[D];南京大学;2014年

2 陈昀林;舰载分布式构件系统的容错技术研究[D];中国舰船研究院;2011年

3 解凯;构件系统回归测试模型与技术研究[D];东南大学;2006年

4 刘伟乾;古文字构件朝向研究[D];华东师范大学;2011年

5 夏辉;基于EJB构件系统的集成测试方法研究[D];西安理工大学;2006年

6 郄晓淼;河北明代长城碑刻文字研究[D];河北师范大学;2015年

本文编号：1043500