节点文献
基于时间着色Petri网的SIP协议验证与分析
Verification and Analysis of SIP Protocol Based on Timed Colored Petri Nets
【摘要】 随着SIP(Session Initiation Protocol)被3G通信选择为下一代移动网络的会话控制机制,保证SIP协议设计和实现无缺陷、运行稳定可靠成为SIP协议应用过程中亟需研究和解决的关键问题。充分利用时间着色Petri网(Timed Colored Petri Nets,TCPN)在描述和分析具有复杂交互行为及时间约束的系统方面的优势,给出了SIP协议的层次TCPN模型,并集成多种模型分析技术,完成SIP协议设计的正确性验证;同时通过正则表达式完成协议模型的生成路径分析,指出其中存在的死锁状态并分析原因。提出了相应的协议设计改进方案,验证了设计方案的正确性,从而有效增强了SIP协议在实际应用中的可行性和可靠性。
【Abstract】 SIP(Session Initiation Protocol)has been selected by 3Gcommunication 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 defect-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 construct 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 effectively improve the feasibility and the reliability for practical SIP applications.
【Key words】 SIP; Timed colored Petri nets; Protocol verification; Deadlock analysis;
- 【文献出处】 计算机科学 ,Computer Science , 编辑部邮箱 ,2014年07期
- 【分类号】TN915.04;TP301.1
- 【下载频次】87