面向复杂随机系统的贝叶斯统计模型检测方法
发布时间：2017-04-09 06:20
本文关键词：面向复杂随机系统的贝叶斯统计模型检测方法，由笔耕文化传播整理发布。
【摘要】：随着网络技术的成熟,加速了各类网络设施、应用和服务的发展,如移动互联网、云计算等。它们渗透进了人们生活的方方面面。越来越多的设施与应用会建立在网络之上。研究如何保证它们的正确性和可靠性就变成一个有意义的课题。不同于其他软硬件系统,网络系统往往包含随机性。虽然业界目前主要采用测试来保证软硬件系统的正确性和可靠性。但是它也存在一些不足,如没有把握保证检测出系统所有的错误和其效果与测试者的经验有较大关联等。为更好地保证复杂随机系统的正确性和可靠性,我们提出了一种基于预测的贝叶斯统计模型检测方法(prediction-based Bayesian model checking)。从模型的初始状态开始,随机从模型中选择一条有限路径,并多次重复这个过程。由于有限路径是相互独立的,因此就能将所有的有限路径看作为样本,并通过贝叶斯推断(Bayesian Inference)来推断模型满足性质的概率。另外,我们利用贝叶斯统计学中先验分布与后验分布的共轭关系,在验证前预测所需样本的数量上限。并且保证一旦抽样数量达到该上限时,当前的结果已经达到了可信度与精度的要求,可立即返回。其次,根据之前所预测的上限,我们会在每次统计数据更新后,再次利用共轭关系来预测所有可能的推断结果。当所有可能的结果都与当前结果一致时,便直接返回结果。为提高对一部分复杂系统的验证效率(运行周期较长的随机系统),我们另外提出了一种启发式的抽样与验证算法。它将路径抽样与路径验证分开成两个阶段：在对路径进行验证时,尝试利用算法来定位一个“可判前缀”,而这个“可判前缀”能够直接用来判定该路径是否满足性质。而在后续的抽样中,根据之前所收集的“可判前缀”信息,便可以直接判断路径是否满足性质。从而避免耗时的路径验证。并且,它还可以与基于预测的贝叶斯统计模型检测算法相结合。SPAC(Statistical Probabilistic Approximate model Checker)是基于上述算法所实现的统计模型检测工具。通过SPAC对调度算法、分布式算法等案例进行研究后,发现在一些场景下,该算法相对于其他统计模型检测算法效率更高。并且对于运行周期较长的系统,启发式算法也可以进一步提高验证效率。
【关键词】：统计模型检测 复杂随机系统 贝叶斯推断 启发式算法 预测 SPAC
【学位授予单位】：华东师范大学
【学位级别】：硕士
【学位授予年份】：2016
【分类号】：O212.8
【目录】：
- 摘要6-8
- ABSTRACT8-15
- 第一章 绪论15-23
- 1.1 研究背景15-18
- 1.2 研究动机18-20
- 1.3 相关工作20-21
- 1.4 文章结构21-23
- 第二章 背景知识23-28
- 2.1 模型定义与性质描述23-25
- 2.1.1 离散时间马尔可夫链与概率迁移系统23
- 2.1.2 事件的测度23-24
- 2.1.3 概率计算树逻辑PCTL24-25
- 2.2 贝叶斯推断25-27
- 2.2.1 贝叶斯推断与先验信息25-26
- 2.2.2 贝叶斯推断过程26-27
- 2.2.3 共轭先验分布定理27
- 2.3 本章小结27-28
- 第三章 基于预测的贝叶斯统计模型检测方法28-57
- 3.1 基本介绍28-29
- 3.2 面向定性性质的验证算法29-38
- 3.2.1 方法框架29-31
- 3.2.2 抽样数量上限预测方法31-33
- 3.2.3 面向定性性质的统计结果预测方法33-35
- 3.2.4 结果可信度计算方法35-36
- 3.2.5 算法描述36-38
- 3.3 面向定量性质的检测算法38-42
- 3.3.1 方法框架38
- 3.3.2 面向定量性质的统计结果预测方法38-40
- 3.3.3 算法描述40-42
- 3.4 启发式抽样与验证算法42-54
- 3.4.1 方法框架42-43
- 3.4.2 一个基本观察43-44
- 3.4.3 最短可判前缀44-49
- 3.4.4 启发式抽样与验证算法49-54
- 3.5 完整算法验证过程54-56
- 3.6 本章小结56-57
- 第四章 统计模型检测工具SPAC57-63
- 4.1 工具介绍57-58
- 4.2 工具实现58-61
- 4.2.1 界面与配置模块59
- 4.2.2 参数检查模块59
- 4.2.3 DTMC模型构建模块59-60
- 4.2.4 PCTL语法解析模块60
- 4.2.5 统计模型检测算法模块60-61
- 4.2.6 有限路径验证模块61
- 4.3 本章小结61-63
- 第五章 案例研究63-83
- 5.1 基本介绍63
- 5.2 简单随机调度算法63-70
- 5.2.1 简单随机调度算法介绍64-65
- 5.2.2 算法正确性评估65-66
- 5.2.3 不同运行周期下的验证效率评估66-67
- 5.2.4 指定不同先验分布时的验证效率评估67-69
- 5.2.5 不同概率阈值下的验证效率评估69-70
- 5.3 同步的领导者选举协议70-76
- 5.3.1 同步的领导者选举协议介绍70
- 5.3.2 面向定量性质的验证效率评估70-72
- 5.3.3 指定不同先验分布时的验证效率评估72-73
- 5.3.4 不同概率阈值下的验证效率评估73-74
- 5.3.5 不同问题规模下的验证效率评估74-76
- 5.4 Herman分布式算法76-81
- 5.4.1 Herman分布式算法介绍76-78
- 5.4.2 面向定量性质的验证效率评估78-79
- 5.4.3 不同运行周期下的验证效率评估79-81
- 5.4.4 复杂问题的验证效率81
- 5.5 本章小结81-83
- 第六章 总结与展望83-85
- 6.1 总结83-84
- 6.2 展望84-85
- 附录A 启发式验证算法中的关键状态定位算法85-88
- 附录B 简单随机调度算法在PRISM中的模型定义88-90
- 附录C 抽样上限预测算法90-92
- 附录D 同步领导者选举协议在PRISM中的模型定义92-96
- 附录E 读硕士学会期间发表论文和科研情况96
- 附录F 参与科研项目情况96-97
- 参考文献97-102
- 致谢102
【相似文献】
中国期刊全文数据库 前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，
本文编号：294656
本文链接：https://www.wllwen.com/kejilunwen/yysx/294656.html
