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

《SIP协议的形式化分析与验证》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、20O9年第1期桂林航天工业高等专科学校学报(总第53期)JOURNALOFGUILINCOLLEGEOFAEROSPACETECHNOLOGY计算机技术及应用SIP协议的形式化分析与验证魏星隋新／1桂林电子科技大学计算机与控制学院，广西桂林541004、＼2挂林航天工业高等专科学校计算机系，广西桂林541004摘要文章在分析SIP会话交互过程的基础上，用petri网对该过程进行建模，根据petri模型所应具备的特性，通过可达树模型验证了SIP协议具有有界性、活性、公平性和前进性。通过不变量分析，验证了SIP协议具有守恒性和循环性。为协议的改进设计提供了理论依据，从而

2、更好完善SIP协议标准。关键词SIP；Petri网；可达树；不变量中图分类号：TP393文献标志码：A文章编号：1OO9—1o33(20O9)o1—0063一o5SIP协议是基于因特网的IP电话信令协议，主要解决功能介绍见表1。IP网中信令控制，SIP协议具有其简单性、可扩展性、可模块化等优点，已成为网络多媒体通信的标准协议，与此同时，为了更好适应IP用户实际增加的应用需求，SIP协议仍在不断完善和扩展，然而随着网络技术的发展，协议设计变得越来越困难，设计过程的任何一个错误都会影响整个协议的稳定性和健壮性。SIP协议已广泛应用到很多领域，人们对SIP协议进行形式化分析

3、和设计，petri网是对协议的进行形式化分析和设计的典型工具，广泛适用于复杂系统的模型建立和性能分析。从对SIP协议的形式化研究情况来看，目前，已经图1SIP协议的系统结构提出对两个终端会话交互的petri网模型和SIP协议的有表1SIP系统元素功能介绍限状态机模型以及用SDL语言描述SIP协议，本文提出一SIP系统元素功能介绍种带有代理服务器参与的SIP会话交互过程的petri网模用户代理分为代理客户机和代理服务器，前者型。发起呼叫请求，后者响应呼叫请求代理服务器将接收到的请求转发给下一跳服务器1SIP协议重定向服务器是个规划呼叫路径的服务器，通过响1．1SIP协议

4、简介应告诉客户下一跳服务器地址SIP协议(SessionInitiationProtocol会话发起协议)是位置服务器用于存储用户端信息一个基于应用层的协议，用来建立、控制维护和终止多媒体会话和呼叫。大范围应用于多媒体通信，支持包括IP电1．3SIP协议会话交互过程话、多媒体会议、远程学习、Internet会话和多媒体发布等SIP协议通过发送，接收消息来连接，建立以及结束会服务。话过程，SIP协议消息分成两类：请求和响应，有6种消息SIP协议通过基于文本的消息包在两个实体之间传递类型：(1)INVITE：用于发起呼叫请求；(2)BYE：会话结消息，在网络上提供代理服务

5、器和重定向服务器来中继和束消息，用于终止会话时使用；(3)OPTION：用于询问被传递消息。叫端的能力信息；(4)ACK：对收到的消息进行确认回答；1．2SIP协议系统结构SIP系统由4种元素组成：用户代理、SIP代理服务器、(5)REGISTER：用于用户向注册服务器传送位置信息和地重定向服务器以及SIP注册服务器，如图1所示，系统元素址信息；(6)CANcLE：取消当前的请求，具体过程见图2。*作者简介：魏星(198O一)，男，四川资中人，桂林航天工业高等专科学校计算机系教师，桂林电子科技大学2007级硕士研究生，研究方向：计算机网络。632009年第1期桂林航天

6、工业高等专科学校学报(总第53期)JOURNALOFGUILINCOLLEGEOFAEROSPACETECHNOLOGY魏星隋新／文网络，PN模型具有直观、形象等优点，有许多优良特性，已广泛用于分布式系统、信息系统、离散事件系统等领域。Petri网结构：是一个三元组N一(P，T，F)，其中，P一{P，P2，⋯，pn)是有限位置集合；T一{t-，t，⋯，t)是有限迁移集合(PUT≠，PnT一)；F(P×T)U(T×P)为流关系。位置集和迁移集是Petri网的基本成分。普通Petri网：普通Petri网形式上定义为一个六元组PN一(P，T，F，MO)一(N，M0)，其中：

7、(1)N一(P，T，F)是一个Petri网结构。(2)M：P—Z(非负整数集合)是位置集合上的标识向量。标识向量M中位置p所对应的分量，称为位置p上的标识或者令牌数目。Mo是初始标识向量。用户代理^代理服务■^S～不变量：I为PN的S一向量，C是PN的关联矩阵，图2SIP协议的会话交互过程若C·I—o，称I为PN的S一不变量。(1)用户代理A发送一个呼叫连接请求消息给用户代T一不变量：J为PN的T一向量，C是PN的关联矩理B，消息发到了代理服务器A。阵，若C·J一0，就称J为PN的T一不变量。(2)代理服务器A将连接请求转发给代理服务器B。Petri