移动自助服务系统通过有线或无线网络实现了对其自助服务终端的远程监视和控制,方便公司内部管理,并且为用户提供了方便的途径完成缴费和其他基础业务。由于系统的复杂性,对于系统的分析和验证显得尤为重要,这时就需要建立一种精确的可模拟系统动态运行的模型。在移动自助服务系统中,与进程交互的外部环境也在动态地改变,具有随机性、动态性、计算的复杂性和应用的广泛性。1992年,英国著名的科学家和图灵奖获得者Robin Miler建立和提出了Pi-演算理论。Pi-演算可以描述结构不断变化的分布式并发系统,是一种新的通信建模方法。所以本文采用了Pi-演算形式化方法为系统建模。本文在对移动自助服务系统的缴费流程进行建模时,采用自顶向下的建模方法,首先在分析系统缴费流程的基础上,提取出其中的主要活动模块,建立顶层的Pi-演算模型；然后细化这些模块,详细地分析每一个模块包含的细节活动,继而得出完整的Pi-演算模型；最后使用Pi-演算的形式化验证工具MWB验证了模型的正确性(如有无死锁),而且用step命令模拟了自助服务系统平台的交互运行情况,可以看出它满足了预期设计的要求。移动自助服务系统所采用的通信协议是TCP/IP协议；本文为了达到对协议进行安全性验证的目的,主要分析了其中的传输控制协议TCP。在分析TCP协议中的数据报格式、连接的建立和释放以及快速重传算法的基础上,对TCP建立连接时采取的三次握手协议建立了Pi-演算模型,并在MWB工具中用step命令模拟了三次握手的动态运行,从理论的角度分析了快速重传机制在建立TCP连接时的应用,给人们控制进程带来很多的益处。本文为系统的缴费流程建立了精确的Pi-演算模型,同时也用Pi-演算理论分析了TCP建立连接的三次握手协议,对系统达成了一致的理解,奠定了系统的分析和改进。