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