| 提要 | 第1-7页 |
| 第一章 引言 | 第7-15页 |
| ·背景简介 | 第7-9页 |
| ·技术发展 | 第9-12页 |
| ·Web Service 及其组合发展现状 | 第9-10页 |
| ·PI-演算发展现状 | 第10-11页 |
| ·移动通信技术发展现状 | 第11-12页 |
| ·本文的主要工作 | 第12-13页 |
| ·本文的结构 | 第13-15页 |
| 第二章 Web Service及其组合 | 第15-28页 |
| ·Web Service 概述 | 第15-19页 |
| ·Web Service | 第15-17页 |
| ·Web Service 特点 | 第17-19页 |
| ·Web Service 模型及体系结构 | 第19-22页 |
| ·Web Service 体系结构中的角色 | 第20-21页 |
| ·Web Service 体系结构中的操作 | 第21页 |
| ·Web Service 的构件 | 第21-22页 |
| ·Web Service 概念性协议栈 | 第22-26页 |
| ·网络层 | 第22-23页 |
| ·基于 XML 消息传递层 | 第23-24页 |
| ·服务描述层 | 第24页 |
| ·Web Service 协议栈综述 | 第24-26页 |
| ·Web Service 组合 | 第26-28页 |
| 第三章 PI-演算概述 | 第28-43页 |
| ·进程代数概述 | 第28-29页 |
| ·PI-演算的发展背景 | 第29-31页 |
| ·PI-演算的基本概念 | 第31-37页 |
| ·PI-演算语法定义及操作语义 | 第32-36页 |
| ·PI-演算结构等价规则与化简规则 | 第36-37页 |
| ·PI-演算与Web Service | 第37-42页 |
| ·PI-演算与Web Service 组合 | 第42-43页 |
| 第四章 PI-演算建模移动通信服务 | 第43-60页 |
| ·建模移动通信连接初始化过程 | 第44-47页 |
| ·建模移动通信过程 | 第47-52页 |
| ·建模移动通信基站转换过程 | 第52-55页 |
| ·建模呼叫重建的基本流程 | 第55-60页 |
| 第五章 PI-演算互模拟定义框架 | 第60-73页 |
| ·Web Service 的可替换性 | 第60-63页 |
| ·Web Service 可替换的充分条件 | 第60-61页 |
| ·用 PI-演算描述Web Service 兼容性 | 第61-62页 |
| ·异步 Web Service 可替换性 | 第62-63页 |
| ·互模拟框架概述 | 第63-64页 |
| ·互模拟定义 | 第64-73页 |
| ·强互模拟等价 | 第64-69页 |
| ·弱互模拟等价 | 第69-73页 |
| 第六章 PI-演算模型的验证 | 第73-85页 |
| ·验证的背景概述 | 第73-74页 |
| ·MWB 概述 | 第74-75页 |
| ·MWB 常用命令解析 | 第75-80页 |
| ·建模与验证 | 第80-85页 |
| ·互模拟验证 | 第80-82页 |
| ·执行步骤验证 | 第82-83页 |
| ·死锁验证 | 第83-85页 |
| 第七章 结语 | 第85-88页 |
| ·工作总结 | 第85页 |
| ·未来工作展望 | 第85-88页 |
| ·实现自动化验证工具 | 第86页 |
| ·PI-网 | 第86-88页 |
| 参考文献 | 第88-92页 |
| 摘要 | 第92-96页 |
| Abstract | 第96-100页 |
| 致谢 | 第100页 |