| 摘要 | 第1-5页 |
| ABSTRACT | 第5-7页 |
| 目录 | 第7-10页 |
| 第一章 绪论 | 第10-24页 |
| ·引言 | 第10-11页 |
| ·研究现状 | 第11-20页 |
| ·事务分类 | 第11-13页 |
| ·事务的形式化研究现状 | 第13-20页 |
| ·事务的实现现状 | 第20页 |
| ·存在问题 | 第20-21页 |
| ·本文的主要工作 | 第21-22页 |
| ·本文的组织 | 第22-24页 |
| 第二章 多元π演算 | 第24-30页 |
| ·引言 | 第24页 |
| ·语法 | 第24-25页 |
| ·迁移语义 | 第25-27页 |
| ·互模拟 | 第27页 |
| ·算子 | 第27-28页 |
| ·MWB工具介绍 | 第28-30页 |
| 第三章 WEB服务原子事务提交协议的形式化描述与模型检验 | 第30-40页 |
| ·引言 | 第30-32页 |
| ·WS-AT协议 | 第32-35页 |
| ·状态转换图和状态转换表 | 第34-35页 |
| ·WS-AT的2PC协议形式化描述 | 第35-36页 |
| ·WS-AT的2PC协议的原子性证明 | 第36-38页 |
| ·本章小结 | 第38-40页 |
| 第四章 WEB服务业务事务协调协议的形式化描述与模型检验 | 第40-54页 |
| ·引言 | 第40页 |
| ·WS-BA协议 | 第40-44页 |
| ·状态转换图和状态转换表 | 第42-44页 |
| ·扩展的BAPC协议 | 第44-46页 |
| ·BAPC的形式化描述 | 第46-47页 |
| ·BAPC模型检验 | 第47-52页 |
| ·持久性 | 第47-49页 |
| ·可终止性 | 第49-50页 |
| ·局部原子性 | 第50-52页 |
| ·本章小结 | 第52-54页 |
| 第五章 事务工作流的实现框架 | 第54-62页 |
| ·引言 | 第54-55页 |
| ·实现框架的原理及组成 | 第55-60页 |
| ·数据结构 | 第55-56页 |
| ·扩展的BPEL语言 | 第56-57页 |
| ·组合验证工具 | 第57-58页 |
| ·工作流引擎 | 第58-59页 |
| ·事务管理与监控器 | 第59页 |
| ·事务协调器 | 第59-60页 |
| ·两种事务管理体系 | 第60页 |
| ·基于实现框架的系统总体结构 | 第60-61页 |
| ·本章小结 | 第61-62页 |
| 第六章 结束语 | 第62-64页 |
| ·论文的主要贡献 | 第62-63页 |
| ·未来进一步的工作 | 第63-64页 |
| 参考文献 | 第64-70页 |
| 附录1 WS-AT协议的2PC协议的状态转换表 | 第70-72页 |
| 附录2 WS-BA的参与者主动提交协议的状态转换表 | 第72-76页 |
| 附录3 WS-BA的协调者主动提交协议的状态转换表 | 第76-80页 |
| 附录4 攻读硕士学位期间发表的学术论文 | 第80-82页 |
| 附录5 致谢 | 第82-84页 |
