基于时间着色Petri网的SIP协议形式化验证与分析

摘要

随着云计算和物联网技术的兴起，联网设备逐渐向移动化、小型化、功能集成化发展，会话初始化协议(SessionInitiationProtocol，SIP)协议以其无缝、灵活、可扩展的特性顺应了技术发展的要求，在许多领域发挥着重要的作用，同时应用领域也随着下一代互联网(NextGenerationNetwork，NGN)的发展而不断扩大。为了适应各种网络环境及SIP应用的需要，须对协议进行必要的扩展、修改和进一步完善。然而技术的发展使得网络协议的开发难度也进一步加大，协议开发过程中任何一点错误和缺陷都将给系统的稳定性、可靠性、安全性等带来巨大的影响。如何较早的发现协议中存在问题，去除风险，降低应用开发和维护成本，是一个值得研究的课题。
　　 为了实现上述目的，采用形式化的方法对协议进行建模以及分析，可以有效的保证协议自身的正确性，无歧义性。一个定义完备验证无误的协议可以有效的减少后期的开发以及维护费用。另外从协议工程的角度看，验证也是一个协议开发生命周期中重要的步骤。时间着色Petri网(TimedColoredPetriNet，TCPN)作为一种形式化建模与分析技术，非常适合描述具有并发行为及时间约束条件的通信系统。目前对SIP的研究很多，但缺少对SIP的形式化验证和模型分析，不能反映出SIP整体的特性，基于层次TCPN对SIP协议进行建模与验证更是不多见。
　　 本文针对这些方面研究的不足，提出了一种基于TCPN的SIP协议状态分层建模方法，指导在不同状态下对协议功能行为进行分层抽象建模。并在该方法的指导下，给出了该协议的层次TCPN模型，准确、直观的描述了协议的主体功能行为。之后，对SIP中的时间约束条件进行了验证，使模型按照协议约束的特定时间进行状态转移与消息交互，保证了模型对协议时间细节的精确刻画。然后，在系统TCPN模型的基础上，集成模拟、状态空间分析和模型检验等技术，在协议模型的不同抽象层次上完成协议分析，验证模型满足协议需求的部分。最后，通过正则表达式完成对模型模拟生成数据的采集过滤，并对协议进行路径分析，指出其中存在的几种死锁状态，针对该死锁造成的可用性问题提出多种解决方案，并对方案的正确性和适用场合进行了验证与说明。
　　 本课题的研究成果为SIP协议标准的不断完善提供了理论分析依据和有效的改进建议，可促进该协议体系的不断发展。