| 摘要 | 第1-8页 |
| ABSTRACT | 第8-15页 |
| 第一章 绪论 | 第15-23页 |
| ·研究背景 | 第15-18页 |
| ·研究动机 | 第18-20页 |
| ·相关工作 | 第20-21页 |
| ·文章结构 | 第21-23页 |
| 第二章 背景知识 | 第23-28页 |
| ·模型定义与性质描述 | 第23-25页 |
| ·离散时间马尔可夫链与概率迁移系统 | 第23页 |
| ·事件的测度 | 第23-24页 |
| ·概率计算树逻辑PCTL | 第24-25页 |
| ·贝叶斯推断 | 第25-27页 |
| ·贝叶斯推断与先验信息 | 第25-26页 |
| ·贝叶斯推断过程 | 第26-27页 |
| ·共轭先验分布定理 | 第27页 |
| ·本章小结 | 第27-28页 |
| 第三章 基于预测的贝叶斯统计模型检测方法 | 第28-57页 |
| ·基本介绍 | 第28-29页 |
| ·面向定性性质的验证算法 | 第29-38页 |
| ·方法框架 | 第29-31页 |
| ·抽样数量上限预测方法 | 第31-33页 |
| ·面向定性性质的统计结果预测方法 | 第33-35页 |
| ·结果可信度计算方法 | 第35-36页 |
| ·算法描述 | 第36-38页 |
| ·面向定量性质的检测算法 | 第38-42页 |
| ·方法框架 | 第38页 |
| ·面向定量性质的统计结果预测方法 | 第38-40页 |
| ·算法描述 | 第40-42页 |
| ·启发式抽样与验证算法 | 第42-54页 |
| ·方法框架 | 第42-43页 |
| ·一个基本观察 | 第43-44页 |
| ·最短可判前缀 | 第44-49页 |
| ·启发式抽样与验证算法 | 第49-54页 |
| ·完整算法验证过程 | 第54-56页 |
| ·本章小结 | 第56-57页 |
| 第四章 统计模型检测工具SPAC | 第57-63页 |
| ·工具介绍 | 第57-58页 |
| ·工具实现 | 第58-61页 |
| ·界面与配置模块 | 第59页 |
| ·参数检查模块 | 第59页 |
| ·DTMC模型构建模块 | 第59-60页 |
| ·PCTL语法解析模块 | 第60页 |
| ·统计模型检测算法模块 | 第60-61页 |
| ·有限路径验证模块 | 第61页 |
| ·本章小结 | 第61-63页 |
| 第五章 案例研究 | 第63-83页 |
| ·基本介绍 | 第63页 |
| ·简单随机调度算法 | 第63-70页 |
| ·简单随机调度算法介绍 | 第64-65页 |
| ·算法正确性评估 | 第65-66页 |
| ·不同运行周期下的验证效率评估 | 第66-67页 |
| ·指定不同先验分布时的验证效率评估 | 第67-69页 |
| ·不同概率阈值下的验证效率评估 | 第69-70页 |
| ·同步的领导者选举协议 | 第70-76页 |
| ·同步的领导者选举协议介绍 | 第70页 |
| ·面向定量性质的验证效率评估 | 第70-72页 |
| ·指定不同先验分布时的验证效率评估 | 第72-73页 |
| ·不同概率阈值下的验证效率评估 | 第73-74页 |
| ·不同问题规模下的验证效率评估 | 第74-76页 |
| ·Herman分布式算法 | 第76-81页 |
| ·Herman分布式算法介绍 | 第76-78页 |
| ·面向定量性质的验证效率评估 | 第78-79页 |
| ·不同运行周期下的验证效率评估 | 第79-81页 |
| ·复杂问题的验证效率 | 第81页 |
| ·本章小结 | 第81-83页 |
| 第六章 总结与展望 | 第83-85页 |
| ·总结 | 第83-84页 |
| ·展望 | 第84-85页 |
| 附录A 启发式验证算法中的关键状态定位算法 | 第85-88页 |
| 附录B 简单随机调度算法在PRISM中的模型定义 | 第88-90页 |
| 附录C 抽样上限预测算法 | 第90-92页 |
| 附录D 同步领导者选举协议在PRISM中的模型定义 | 第92-96页 |
| 附录E 读硕士学会期间发表论文和科研情况 | 第96页 |
| 附录F 参与科研项目情况 | 第96-97页 |
| 参考文献 | 第97-102页 |
| 致谢 | 第102页 |