面向服务的多参与者协调建模验证
| 摘要 | 第1-5页 |
| Abstract | 第5-8页 |
| 图表清单 | 第8-10页 |
| 注释表 | 第10-11页 |
| 第一章 绪论 | 第11-16页 |
| ·课题研究背景及意义 | 第11-12页 |
| ·Web 服务事务研究现状与发展 | 第12-14页 |
| ·论文研究内容和组织结构 | 第14-16页 |
| 第二章 Web 服务事务问题描述 | 第16-25页 |
| ·Web 服务事务特性 | 第16-17页 |
| ·Web 服务事务处理协议 | 第17-22页 |
| ·Web 服务协调 | 第17-18页 |
| ·Web 服务原子事务 | 第18-20页 |
| ·Web 服务业务活动 | 第20-22页 |
| ·Web 服务事务的形式化研究 | 第22-24页 |
| ·基于Petri 网的形式化方法 | 第22-23页 |
| ·基于自动机理论的形式化方法 | 第23页 |
| ·基于进程代数的形式化方法 | 第23-24页 |
| ·本章小结 | 第24-25页 |
| 第三章 Web 服务多参与者协调建模 | 第25-44页 |
| ·Pi-演算建模分析 | 第25-26页 |
| ·Web 服务多参与者的协调模型 | 第26-34页 |
| ·参与者模型 | 第26-28页 |
| ·协调器模型 | 第28-34页 |
| ·多参与者协调的Pi-演算建模规则 | 第34-38页 |
| ·多参与者协调和Pi-演算元素映射关系 | 第34-36页 |
| ·BPEL 业务流程的协调建模 | 第36-38页 |
| ·多参与者协调建模算法 | 第38-43页 |
| ·本章小结 | 第43-44页 |
| 第四章 Web 服务多参与者协调性质规约 | 第44-52页 |
| ·计算树逻辑 | 第44-46页 |
| ·多参与者协调性质 | 第46-48页 |
| ·安全性 | 第46-47页 |
| ·活性 | 第47-48页 |
| ·多参与者协调性质形式化规约 | 第48-51页 |
| ·安全性形式化描述 | 第48-50页 |
| ·活性形式化描述 | 第50-51页 |
| ·本章小结 | 第51-52页 |
| 第五章 Web 服务多参与者协调模型检验 | 第52-65页 |
| ·基于NuSMV 的模型检验方法 | 第52-53页 |
| ·检验框架设计与实现 | 第53-59页 |
| ·文本转换工具 | 第54-58页 |
| ·反例分析器 | 第58-59页 |
| ·多参与者协调实例验证 | 第59-64页 |
| ·机票预订服务实例 | 第59-60页 |
| ·机票预订服务协调模型 | 第60-62页 |
| ·机票预订服务协调性质规约 | 第62-63页 |
| ·模型检验结果分析 | 第63-64页 |
| ·本章小结 | 第64-65页 |
| 第六章 总结与展望 | 第65-67页 |
| ·论文工作总结 | 第65页 |
| ·进一步的工作 | 第65-67页 |
| 参考文献 | 第67-70页 |
| 致谢 | 第70-71页 |
| 在学期间的研究成果及发表的学术论文 | 第71-72页 |
| 附录 | 第72-78页 |
| 附录1 机票预订SMV 程序代码 | 第72-76页 |
| 附录2 机票预订模型检验结果 | 第76-78页 |
