基于概率模型检测的生存性分析与验证方法研究
| 摘要 | 第1-5页 |
| Abstract | 第5-7页 |
| 目录 | 第7-9页 |
| 1 绪论 | 第9-13页 |
| ·研究背景 | 第9-10页 |
| ·研究现状 | 第10-11页 |
| ·研究内容 | 第11-12页 |
| ·论文组织结构 | 第12-13页 |
| 2 模型检测技术 | 第13-18页 |
| ·模型检测的定义 | 第13-15页 |
| ·模型检测的特点 | 第15页 |
| ·模型检测的难题及优化技术 | 第15-18页 |
| 3 概率模型检测 | 第18-25页 |
| ·离散马尔科夫链模型 | 第18-20页 |
| ·连续马尔科夫模型 | 第20-22页 |
| ·概率时间自动机模型 | 第22-24页 |
| ·本章小结 | 第24-25页 |
| 4 基于模型检测的生存性分析 | 第25-34页 |
| ·生存性定义及验证方法 | 第25-26页 |
| ·电话接入网的生存性分析 | 第26-29页 |
| ·实验分析 | 第29-32页 |
| ·PRISM简介 | 第29-30页 |
| ·模型与生存性描述 | 第30-31页 |
| ·实验结果 | 第31-32页 |
| ·本章小结 | 第32-34页 |
| 5 带补偿约束的概率模型检测 | 第34-44页 |
| ·带补偿约束的DTMC | 第34-35页 |
| ·描述补偿的LTL_x逻辑 | 第35-37页 |
| ·反例及生成方法 | 第37-42页 |
| ·修改DTMC | 第38页 |
| ·DTMC转换成权重图 | 第38-40页 |
| ·最小反例生成算法 | 第40-42页 |
| ·本章小结 | 第42-44页 |
| 6 总结与展望 | 第44-46页 |
| ·论文总结 | 第44-45页 |
| ·论文的不足和展望 | 第45-46页 |
| 参考文献 | 第46-50页 |
| 致谢 | 第50-51页 |
| 个人简历及发表论文情况 | 第51页 |
| 个人简历 | 第51页 |
| 硕士期间发表论文 | 第51页 |
