移动通信系统中移动性管理的形式化描述与验证

摘要

随着数字通信，计算机以及网络技术的发展，移动通信凭借其自身方便便捷的特点，呈现出如火如茶的发展势态。移动通信的目的是为了实现任何时间、任何地点和任何通信对象之间的通信。与固定通信系统显著不同的一点是：移动台的位置是不断变化的。这使得移动性管理成为一个重点。
　　 移动性管理通过位置管理中的双层数据库结构实现。所有移动台的位置信息都存储在双层数据库中。随着移动台位置的不断变化，为完成对移动台的呼叫、数据传输等请求，需要不断更新对应的数据库中的位置信息。由于移动台位置变化而引发的后续流程，跟移动台的状态有关。若移动台是在开机空闲状态下移动的，只需及时进行位置更新。而若移动台是在通话状态下移动的，需要切换流程来确保通话不被中断。并在此次通信结束后进行位置更新。
　　 本文详细地研究了移动通信系统中的移动性管理，运用Pi-演算对GSM中的双层数据库架构进行了形式化描述，得到了简化系统模型。文中提出了移动通信系统必须满足的两个重要性质：移动台的可移动性和系统的移动无关性，并对它们进行了形式化描述。然后，通过手动推演的方法，我们证明了简化系统模型是能够满足这两个性质的，因此是正确的。最后，为进一步检验模型的正确性，我们还使用模型检测工具对简单模型的描述进行了语法检测和死锁检测。

目录

文摘

英文文摘

声明

第一章 引言

1.1 背景简介

1.2 研究现状

1.2.1 移动性管理研究现状

1.2.2 Pi-演算发展现状

1.3 本文的主要研究工作

1.4 本文的组织结构

第二章 背景知识

2.1 移动通信系统的网络结构

2.1.1 GSM网络体系结构

2.1.2 GPRS体系结构

2.1.3 UMTS网络结构

2.2 移动性管理

2.3 Pi-演算基本理论

2.3.1 进程代数概述

2.3.2 Pi-演算的语法

2.3.3 Pi-演算的操作语义

2.3.4 Pi-演算的互模拟等价关系

2.3.5 移动性

2.4 模型检测工具MWB

2.5 小结

第三章 Pi-演算建模移动通信系统

3.1 各部分的模型

3.1.1 MS的模型

3.1.2 MSC/VLR的模型

3.1.3 HLR的模型

3.2 简化后的移动通信系统

3.3 小结

第四章 相关性质及验证

4.1 移动性

4.2 移动不相关性

4.3 小结

第五章 移动通信系统的模型检测

5.1 用MWB检测语法定义

5.2 用MWB检测结构死锁

5.3 用MWB检验通信流程

5.4 小结

第六章 总结与展望

6.1 总结工作

6.2 未来展望

附录A MWB代码

参考文献

攻读硕士学位期间的研究成果

致谢