| 摘要 | 第4-5页 |
| Abstract | 第5页 |
| 第一章 绪论 | 第8-13页 |
| 1.1 研究背景 | 第8-10页 |
| 1.2 研究现状 | 第10-11页 |
| 1.3 论文工作 | 第11页 |
| 1.4 论文组织结构 | 第11-13页 |
| 第二章 移动云计算与服务转移的相关概念和技术 | 第13-26页 |
| 2.1 移动云计算的概念 | 第13页 |
| 2.2 云计算的服务形式及其相关技术 | 第13-18页 |
| 2.2.1 云计算的服务形式 | 第13-14页 |
| 2.2.2 云计算的相关技术 | 第14-18页 |
| 2.3 移动云计算 | 第18-20页 |
| 2.3.1 移动云计算架构的出现 | 第18-19页 |
| 2.3.2 移动云计算的应用 | 第19-20页 |
| 2.4 服务转移的实现技术 | 第20-24页 |
| 2.4.1 OSGi概述 | 第20-22页 |
| 2.4.2 OSGi的服务管理过程 | 第22-23页 |
| 2.4.3 R-OSGi | 第23页 |
| 2.4.4 移动云服务中的OSGi | 第23-24页 |
| 2.5 移动云计算发展过程中的挑战 | 第24页 |
| 2.6 本章小结 | 第24-26页 |
| 第三章 形式化方法与Event-B模型验证 | 第26-37页 |
| 3.1 形式化方法 | 第26-30页 |
| 3.1.1 形式化方法的应用形式 | 第28-29页 |
| 3.1.2 可以用于做形式化方法的系统与证明 | 第29-30页 |
| 3.2 Event-B基本概念 | 第30-32页 |
| 3.3 Event-B语言 | 第32-36页 |
| 3.3.1 Contexts（环境） | 第32-33页 |
| 3.3.2 Machines（机器） | 第33-34页 |
| 3.3.3 Events（事件） | 第34-35页 |
| 3.3.4 Refine（精化） | 第35-36页 |
| 3.4 本章小结 | 第36-37页 |
| 第四章 移动云环境下的建模精化与验证 | 第37-53页 |
| 4.1 移动云环境下服务转移系统需求分析 | 第37-40页 |
| 4.2 使用Event-B对移动云环境下服务转移系统进行建模 | 第40-52页 |
| 4.2.1 系统的初始化模型 | 第40-42页 |
| 4.2.2 服务请求与转移过程模型的建立 | 第42-50页 |
| 4.2.3 服务请求与转移过程模型的验证 | 第50-52页 |
| 4.3 本章小结 | 第52-53页 |
| 第五章 服务转移系统的设计与实现 | 第53-61页 |
| 5.1 系统的整体设计 | 第53-58页 |
| 5.1.1 系统的整体设计思路 | 第53-54页 |
| 5.1.2 系统的整体框架 | 第54页 |
| 5.1.3 MCSTS中的Master选举的实现 | 第54-56页 |
| 5.1.4 MCSTS的详细设计与实现 | 第56-58页 |
| 5.2 MCSTS系统实验验证 | 第58-60页 |
| 5.3 本章小结 | 第60-61页 |
| 总结与展望 | 第61-63页 |
| 研究工作与创新点 | 第61页 |
| 未来与展望 | 第61-63页 |
| 参考文献 | 第63-67页 |
| 致谢 | 第67页 |