基于Pi-演算的移动自助服务系统的建模与验证
| 摘要 | 第3-4页 |
| Abstract | 第4页 |
| 第一章 引言 | 第7-11页 |
| 1.1 课题的研究背景及意义 | 第7-8页 |
| 1.2 国内外研究状况及发展趋势 | 第8-10页 |
| 1.2.1 移动自助服务系统的发展和研究现状 | 第8-9页 |
| 1.2.2 Pi-演算建模理论的发展及研究现状 | 第9-10页 |
| 1.3 本文的研究工作和框架结构 | 第10-11页 |
| 第二章 基础理论介绍 | 第11-20页 |
| 2.1 并发系统建模方法 | 第11-12页 |
| 2.1.1 并发系统的概念 | 第11页 |
| 2.1.2 形式化方法 | 第11-12页 |
| 2.2 Pi-演算的基本理论 | 第12-18页 |
| 2.2.1 Pi-演算的特点 | 第12-14页 |
| 2.2.2 Pi-演算的语法 | 第14-15页 |
| 2.2.3 Pi-演算的结构等价 | 第15-16页 |
| 2.2.4 Pi-演算的操作语义 | 第16-18页 |
| 2.3 本章小结 | 第18-20页 |
| 第三章 移动自助服务系统分析 | 第20-26页 |
| 3.1 移动自助服务系统的网络结构 | 第20-22页 |
| 3.2 移动自助服务系统的技术组成 | 第22-24页 |
| 3.3 移动自助服务系统的效用和效率分析 | 第24-25页 |
| 3.4 本章小结 | 第25-26页 |
| 第四章 缴费流程的Pi-演算模型及其验证 | 第26-39页 |
| 4.1 移动自助服务系统的缴费流程 | 第26-29页 |
| 4.1.1 缴费流程图 | 第26-27页 |
| 4.1.2 顶层的缴费流程模型 | 第27-28页 |
| 4.1.3 完整的缴费流程模型 | 第28-29页 |
| 4.2 移动自助服务系统缴费流程的Pi-演算模型 | 第29-32页 |
| 4.2.1 顶层缴费流程的Pi-演算模型 | 第29-30页 |
| 4.2.2 完整缴费流程的Pi-演算模型 | 第30-32页 |
| 4.3 验证系统缴费流程的Pi-演算模型 | 第32-37页 |
| 4.3.1 MWB中的Pi-演算建模语法 | 第32-33页 |
| 4.3.2 MWB公式语义 | 第33-34页 |
| 4.3.3 模型检测 | 第34-37页 |
| 4.4 本章总结 | 第37-39页 |
| 第五章 基于Pi-演算的TCP协议的建模与验证 | 第39-47页 |
| 5.1 HTTP协议概述 | 第39-40页 |
| 5.2 TCP协议概述 | 第40-44页 |
| 5.2.1 TCP协议数据报的格式 | 第40-41页 |
| 5.2.2 TCP连接的建立 | 第41-42页 |
| 5.2.3 TCP连接的释放 | 第42-44页 |
| 5.2.4 TCP协议的快速重传 | 第44页 |
| 5.3 TCP协议连接建立的Pi-演算描述与验证 | 第44-46页 |
| 5.4 本章总结 | 第46-47页 |
| 第六章 结语 | 第47-48页 |
| 6.1 全文总结 | 第47页 |
| 6.2 进一步的工作 | 第47-48页 |
| 参考文献 | 第48-50页 |
| 致谢 | 第50-51页 |
| 个人简历 | 第51页 |
