基于抽象和学习的统计模型检测研究
发布时间：2017-08-12 15:38
本文关键词：基于抽象和学习的统计模型检测研究
更多相关文章： 信息物理融合系统 随机混成自动机 主成分分析 统计抽象 统计模型检测
【摘要】：信息物理融合系统(Cyber Physical Systems, CPS)是一种更关注计算机与物理环境交互和协作的高级嵌入式系统,自2006年此概念被提出以来,已受到了学术界与工业界的高度关注。第一,CPS应用大都安全攸关或功耗要求严苛,在保证功能的前提下,仍必须满足一定的非功能属性,如吞吐量、能耗等,因此需要验证分析以保证其可信性；第二,CPS大都是异构的混成系统,融合了连续的物理过程和离散的系统行为,且处于高度不确定的开放环境中,因此使用传统的方法(如模型检测和定理证明)难以完成验证分析。为缓解此问题,人们开始尝试使用统计算法对系统模型的仿真Trace进行分析,求得近似结果,并给出结果的误差范围，这种方法被称为统计模型检测(Statistical Model Checking, SMC)。SMC无需遍历状态空间,但当结果精度要求较高时需要产生大量Trace(多数仿真软件的Trace生成比较耗时),性能因此大大降低,本文即针对SMC的性能问题展开深入研究。首先,对已有SMC算法的原理进行了剖析,实现了4种SMC算法,通过大量实验给出了详细的性能评估。基于实验结论,提出了一个自适应的SMC算法框架,以根据不同属性的预估概率,动态地选择合适的SMC算法。其次,为改进自适应的SMC中贝叶斯区间估计算法的不足,提出了基于抽象和学习的SMC方法,旨在减少统计分析所需的Trace数量以提高SMC的效率。其中结合已有的抽象和学习理论(如主成分分析、随机文法推断),对随机混成自动机的仿真Trace进行了概率等价抽象和简化；并基于抽象Trace学习出概率等价的系统行为模型-—前缀频率树,同时提出了树的两阶段约减算法,以有效控制树的规模,为更高效的SMC验证分析提供了良好的抽象模型。最后,介绍了我们实现的CPS建模分析平台-—Modana,基于此平台实现了本文提出的SMC改进算法,基于Modana平台建模分析了典型的CPS系统-—智能温控系统；并结合3个基准测试案例,对SMC算法改进前后的性能和准确度进行了实验性评估。结果证明,本文提出的SMC改进方法正确并且有效。
【关键词】：信息物理融合系统 随机混成自动机 主成分分析 统计抽象 统计模型检测
【学位授予单位】：华东师范大学
【学位级别】：硕士
【学位授予年份】：2016
【分类号】：O212.1;TP273
【目录】：
- 摘要6-7
- ABSTRACT7-12
- 第一章 绪论12-21
- 1.1 研究背景及意义12-14
- 1.2 国内外研究现状14-18
- 1.2.1 CPS的形式化建模14-15
- 1.2.2 统计模型检测15-17
- 1.2.3 基于学习的统计模型检测17-18
- 1.3 本文研究内容18-19
- 1.4 本文组织结构19-20
- 1.5 本章小结20-21
- 第二章 预备知识与概念21-26
- 2.1 随机行为21-22
- 2.2 随机混成自动机22-24
- 2.3 概率有界线性时态逻辑24-25
- 2.4 本章小结25-26
- 第三章 统计模型检测算法的分析与集成26-43
- 3.1 统计模型检测算法的原理剖析27-33
- 3.1.1 定性类SMC算法28-31
- 3.1.2 定量类SMC算法31-33
- 3.2 统计模型检测算法的性能评估33-39
- 3.2.1 关于SMC算法性能的讨论33-34
- 3.2.2 定性类SMC算法34-36
- 3.2.3 定量类SMC算法36-39
- 3.3 自适应的统计模型检测框架39-42
- 3.4 本章小结42-43
- 第四章 基于抽象和学习的统计模型检测43-64
- 4.1 抽象阶段Ⅰ：基于属性的投影45-48
- 4.2 学习及抽象阶段Ⅱ：基于主成分分析的特征降维48-50
- 4.3 抽象阶段Ⅲ：关键点抽取50-52
- 4.3.1 启发式优化过程(可选)52
- 4.4 学习阶段Ⅳ：前缀频率树的构建与约简52-59
- 4.4.1 进一步构建概率有限自动机(可选)55-59
- 4.5 最终概率的统计分析59-61
- 4.6 算法正确性与复杂度分析61-62
- 4.7 本章小结62-64
- 第五章 基于Modana平台的SMC实现64-71
- 5.1 Modana平台概述64-65
- 5.2 AL-SMC算法实现65-69
- 5.2.1 类与函数65-68
- 5.2.2 执行流程与界面展示68-69
- 5.3 本章小结69-71
- 第六章 案例分析与实验评估71-81
- 6.1 智能温控系统的建模与分析71-76
- 6.1.1 系统模型的建立73-75
- 6.1.2 不舒适度与能耗分析75-76
- 6.2 AL-SMC的性能和准确度评估76-79
- 6.3 本章小结79-81
- 第七章 总结与展望81-83
- 参考文献83-90
- 致谢90-91
- 发表论文和科研情况91
【相似文献】
中国期刊全文数据库 前10条
1 陈清亮;朱可宜;;多智能体协同的认知规范模型检测算法[J];中山大学学报(自然科学版);2009年01期
2 周从华;邢支虎;刘志锋;王昌达;;马尔可夫决策过程的限界模型检测[J];计算机学报;2013年12期
3 吉猛;胡克瑾;;基于模型检测的电子商务鉴证技术[J];陕西师范大学学报(自然科学版);2006年04期
4 宁正元;胡山立;赖贤伟;;交互时态信念逻辑及其模型检测[J];南京大学学报(自然科学版);2008年02期
5 王曦;徐中伟;梅萌;;基于模型检测的软件安全性验证方法[J];武汉大学学报(理学版);2010年02期
6 王晶;张广泉;;基于概率时间自动机的模型检测反例表示研究[J];苏州大学学报(自然科学版);2011年02期
7 高妍妍;李曦;周学海;;L4进程间通信机制的模型检测方法[J];中国科学院研究生院学报;2011年06期
8 王扣武;张s，
本文编号：662384
本文链接：https://www.wllwen.com/kejilunwen/zidonghuakongzhilunwen/662384.html
