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

Verification and Analysis of SIP Protocol Based on Timed Colored Petri Nets

作　　者：刘靖[1] 叶新铭[1] 马元飞[1] 

机构地区：[1]内蒙古大学计算机学院,呼和浩特010021

出　　处：《计算机科学》2014年第7期122-129,共8页Computer Science

基　　金：国家自然科学基金项目(61262017);高校博士学科点专项科研基金(20101501110003);内蒙古自然科学基金重点项目(20080404Zd20);内蒙古大学高层次人才引进基金项目资助

摘　　要：随着SIP(Session Initiation Protocol)被3G通信选择为下一代移动网络的会话控制机制,保证SIP协议设计和实现无缺陷、运行稳定可靠成为SIP协议应用过程中亟需研究和解决的关键问题。充分利用时间着色Petri网(Timed Colored Petri Nets,TCPN)在描述和分析具有复杂交互行为及时间约束的系统方面的优势,给出了SIP协议的层次TCPN模型,并集成多种模型分析技术,完成SIP协议设计的正确性验证;同时通过正则表达式完成协议模型的生成路径分析,指出其中存在的死锁状态并分析原因。提出了相应的协议设计改进方案,验证了设计方案的正确性,从而有效增强了SIP协议在实际应用中的可行性和可靠性。SIP（Session Initiation Protocol） has been selected by 3G communication as a session control mechanism for the next generation mobile network, so it is quite significant to ensure that the protocol design and implementation is de- fect-free and runs steadily and reliably. Timed Colored Petri Nets（TCPN） has advantages of modeling and analyzing software systems with complicated and time-constrained behaviors. Thus,TCPN was well adopted in this paper to con- struct a hierarchical formal model for SIP protocol, and several model analysis techniques were used together to validate its design accuracy. Then, using regular expression, the model based protocol execution paths were completely analyzed, and certain deadlock scenarios were pointed out. Finally, we proposed novel and validated protocol design revisions to ef- fectively improve the feasibility and the reliability for practical SIP applications.

关 键 词：SIP 时间着色Petri网 协议验证 死锁分析 

分 类 号：TP319[自动化与计算机技术—计算机软件与理论]