SIP协议的形式化分析与验证

摘要：

文章在分析SIP会话交互过程的基础上,用petri网对该过程进行建模,根据petri模型所应具备的特性,通过可达树模型验证了SIP协议具有有界性、活性、公平性和前进性.通过不变量分析,验证了SIP协议具有守恒性和循环性.为协议的改进设计提供了理论依据,从而更好完善SIP协议标准.

关键词：SIP、Petri网、可达树、不变量

所属期刊栏目：14

分类号：TP393(计算技术、计算机技术)

在线出版日期：2009-05-25（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：63-67