| 摘要 | 第3-5页 |
| Abstract | 第5-6页 |
| 第1章 绪论 | 第9-16页 |
| 1.1 研究背景及意义 | 第9-10页 |
| 1.2 国内外研究现状 | 第10-13页 |
| 1.2.1 Petri网方法 | 第10-11页 |
| 1.2.2 进程代数方法 | 第11页 |
| 1.2.3 有限状态机方法 | 第11-12页 |
| 1.2.4 时态认知逻辑模型检测方法 | 第12-13页 |
| 1.3 本文研究内容与创新点 | 第13-14页 |
| 1.4 论文结构 | 第14-16页 |
| 第2章 模型检测 | 第16-25页 |
| 2.1 Kripke结构 | 第16-17页 |
| 2.2 时态逻辑 | 第17-19页 |
| 2.2.1 线性时态逻辑LTL | 第17-18页 |
| 2.2.2 计算树逻辑CTL* | 第18-19页 |
| 2.3 知识推理 | 第19-21页 |
| 2.4 时态认知逻辑CTLKD | 第21-23页 |
| 2.5 模型检测工具VerICS | 第23-24页 |
| 2.6 本章小结 | 第24-25页 |
| 第3章 Web服务业务流程 | 第25-29页 |
| 3.1 Web服务及其体系结构 | 第25-26页 |
| 3.1.1 Web服务定义 | 第25页 |
| 3.1.2 Web服务体系结构 | 第25-26页 |
| 3.2 Web服务组合 | 第26-27页 |
| 3.3 Web服务业务流程执行语言BPEL | 第27-28页 |
| 3.3.1 BPEL定义 | 第27页 |
| 3.3.2 BPEL组成 | 第27页 |
| 3.3.3 BPEL活动介绍 | 第27-28页 |
| 3.4 本章小结 | 第28-29页 |
| 第4章 BPEL形式模型及其自动化模型检测方法 | 第29-65页 |
| 4.1 BPEL时间约束属性的扩展 | 第29-31页 |
| 4.2 BPEL形式模型BIOSTS | 第31-32页 |
| 4.3 BPEL活动形式化建模 | 第32-50页 |
| 4.3.1 BEPL基本活动形式化建模 | 第32-41页 |
| 4.3.2 BPEL结构活动形式化建模 | 第41-50页 |
| 4.4 BPEL流程自动化模型检测方法 | 第50-60页 |
| 4.4.1 BPEL到BIOSTS转化算法 | 第50-55页 |
| 4.4.2 BIOSTS到IL转化算法 | 第55-60页 |
| 4.5 Web服务组合建模与验证框架 | 第60-64页 |
| 4.5.1 时态认知逻辑ECTLKD与TECTLK | 第61-62页 |
| 4.5.2 框架结构 | 第62-64页 |
| 4.6 本章小结 | 第64-65页 |
| 第5章 实例研究 | 第65-76页 |
| 5.1 VTA概述 | 第65页 |
| 5.2 BPEL时间约束属性扩展 | 第65-67页 |
| 5.3 将 BPEL 转化为 BIOSTS | 第67-69页 |
| 5.4 将BIOSTS转化为IL | 第69-73页 |
| 5.5 VTA规范验证 | 第73-75页 |
| 5.6 本章小结 | 第75-76页 |
| 第6章 总结与展望 | 第76-78页 |
| 参考文献 | 第78-83页 |
| 致谢 | 第83-84页 |
| 个人简历、在学期间发表的学术论文及研究成果 | 第84页 |