论文：SIP协议系统模型的形式化研究.doc

SIP协议系统模型的形式化研究0 引言随着通信技术的快速发展，网络通信技术的要求不断提高，在通信技术中具有决定作用的通信协议的功能也不断完善且更加复杂。ITU-T的Z.100建议SDL(Specification and Description Language)语言可以定义通信协议的分层结构和协议各部分间的相互联系及接口，使用SDL语言描述、分析通信协议，能够提高通信软件开发效率和可靠性。SIP(Session Initiation Protocol)是由IETF提出的在IP网络上进行多媒体通信的控制层协议，SIP被描述为用来生成、修改和终结一个或多个参与者之间的会话。该文首先总结SIP协议系统结构，然后采用SDL来描述SIP协议的系统模型，并对一些特殊情况进行了模拟，验证了SIP协议形式化描述的正确性。1 SIP协议结构1.1 SIP系统组成从结构和功能上划分，SIP系统分为两个部分：SIP客户端(SIP Clients)和SIP服务器(SIP Servers)。SIP Clients主要指用户代理UA(User Agent)，它可以细划为2个部分：用户代理客户端UAC(User AgentClient)，主要用来发起SIP请求；用户代理服务器(User Agent Server)，其作用是：当一个SIP请求收到的时候联系用户并做出基于用户的响应。SIP Servers主要包括注册服务器RS(Registrar Server)，用来处理来自UAC的请求注册用户的位置信息；代理服务器PS(Proxy Server)，它是一种中介设置，主要用来接收一个客户端的请求并继续向前传递该请求，基本上，代理服务器接收SIP消息，然后转发到下一个SIP服务器，代理服务器也可以提供一些机制，例如鉴权、授权、网络接口控制、路由、传播的可靠性及安全性等问题；重定向服务器ReS(Redirect Server)，用来给用户提供下一跳的信息或消息应该经过的跳数，使用户可以直接联系下一跳或直接和目标客户端联系。另外，在一个扩展的SIP系统中，SIP服务器还包括LDAP(LightweightDirectory Access Protocol)服务器、位置服务器LS(Location Servers)、数据库服务器(Database Servers)、XML服务器(Extensible Markup Language)等。1.2 典型SIP系统SIP系统分为四种类型结构：SIP注册结构在此系统结构中包含两个实体：UA和RS，用户代理需要在RS上进行注册以确定自己的身份，把自己连入网络。SIP端到端结构在此系统结构中包含两个对等实体：UA1和UA2，它是双方直接进行通信的简单实例。代理模式结构在此系统结构中包含四个实体：两个UA，LS和PS，UA1向PS发出会话请求，然后PS向LS查询UA2的信息并向UA2发出会话请求，UA2向PS回复确认信息，PS给UA1回复确认信息，UA1向给UA2发确认信息，然后开始通话，任何一方可终止会话，并给对方发出终止消息。 重定向模式结构在此系统结构中包含四个实体：两个UA，LS和PS，UA1向PS发出会话请求，然后PS向LS查询UA2的信息，PS给UA1回复UA2的信息，UA1给UA2发会话邀请信息，UA2给UA1发确认信息，然后开始通话，任何一方可终止停止会话，并给对方发出终止消息。2 SIP协议系统模型的形式化描述SDL语言能够对协议提供规范的、无二异性的描述，用它来描述复杂协议系统的结构可以保证协议描述的正确性和可靠性。用SDL语言描述的系统一般包括4个等级：系统，功能块，进程和代码段。在进程中用扩展状态机详细地描述系统的动态行为，利用时间和定时器描述不同功能块之间通信接口的抽象模型利用信道信号描述通信的处理过程。2.1 SIP协议主要系统模型 SIP协议使用广泛，由它本身组成的系统或与其他协议组成的通信系统比较多，由于篇幅有限，仅列出SIP代理系统模型。在SIP代理系统模型中，其主要功能块分为UA，PS和LS。其中UA组件是会话客户端，是用来发起会话请求、接受请求并回复、进行通话的实体；PS用来转发UA的请求和回复及向LS查询位置信息并结合会话请求回复邀请的客户端，另外还提供一些其他的服务代理等；LS主要提供UA的位置信息，如图1所示。2.2 SIP协议系统模型主要功能块在SIP系统模型中，主要包含UA功能块，PS功能块，LS功能块，RS功能块等。由于篇幅有限，仅列出UA功能块和PS功能块的形式化工作。2.2.1 SIP UA功能块SIP UA功能块包含四个进程块，事务处理控制进程通过保持一系列SIP命令和回应列表命令进行事务处理的管理，当SIP命令被发往其他组件时，它通过给时间控制进程发送一个时间开始消息启动一个定时器。当收到由它发出的SIP命令的其他组件最终回应消息时，它发送一个停止消息给定时器。时间控制进程主要维持定时器，当一个定时器超时或者终止时，它发送超时和终止消息给事务处理控制进程。媒体控制进程控制媒体流的传输。命令控制进程维持整个会话的状态。该功能块有三个外部接口：Transaction_UAroute主要是UA与服务器的事务处理接口；UAController_channel是UA与服务器和UA之间的命令控制事务处理接口；Media_media_route主要指UA之间的媒体流传输接口。图2显示了SIP UA功能块。在图3中给出SIP UA功能块的状态机，主要包括四个状态：IDLE，WAIT_RESPONSE，WAIT_ACK，CONNECTED。IDLE为用户代理初始状态，代表一个会话建立前或结束后的状态，在此状态下，通过INTIVE进程发出会话邀请进入到WAIT_RE-SPONSE状态，其他的状态通过撤销或终止进程回到本状态，自身也可通过RESPONSE进程报错或报告成功。WAIT_RESPONSE为等待回复状态，它表示一个用户代理发出会话邀请后的等待回应状态，它可以通过RESPONSE进程报告错误回到IDLE状态，通过确认ACK进程进入CONNECTED状态，一些振铃进程请求时该状态不变。WAIT_ACK为等待确认媒体信道连接状态，表示当一些请求发出后的等待回复状态。CONNECTED为会话建立成功状态，表示用户代理完成三次握手后成功建立会话的状态，可以通过终止回到初始状态。 2.2.2 SIP Proxy功能块SIP Proxy UA功能块包含三个进程块，事物处理控制进程也通过一系列SIP命令和回应列表进行事务处理的管理，它也可以通过发送控制信息来启动和关闭时间控制进程中的定时器。时间控制进程用于维护时间信息。命令控制进程用来维持用户注册信息、把SIP消息从一个SIP客户端传到另一个SIP客户端等。SIP Proxy功能块，如图4所示，该功能块有两个外部接口，Transaction_proxy_route主要是Proxy与其他实体的事务处理接口；proxy_Controller_channel是Proxy与其他实体服务器活UA之间的命令控制事务处理接口。利用这些接口与其他组件进行通信。SIP Proxy功能块的进程状态机和UA一样，主要包括三个状态：IDLE，WAIT_RESPONSE，WAITACK。IDLE为服务器的初始状态，通过继传源用户代理的INTIVE进程向目标用户代理发出会话邀请进入到WAIT_RESPONSE状态，其他的状态通过撤销或终止进程回到本状态，经过处理后继传给相应的用户代理。WAIT_RESPONSE为等待回复状态，它表示一个命令发出后的等待回应状态，它可以通过RESPONSE进程报告错误回到IDLE状态，一些振铃进程请求时该状态不变。WAIT_ACK为等待确认信道连接状态，表示当一些请求发出后的等待回复状态。2.3 形式化SIP系统模型的模拟与验证为了显示系统不同部件间的交互，使用消息顺序图(Message Sequence Charts，MSC)的消息流形式来验证系统模型的通信，一个MSC图包含系统各部分之间的行为。一组MSC图可以提供一个系统的详细的形式化描述。MSC中语言构造包括实例，消息，环境，行为，定时器设置、重设及超时，实例创建及停止和条件。标准MSC语言为用SDL描述一个SDL系统内部及不同的功能块之间的通信提供了一个强大的支持。MSC可以用来进行规格说明、模拟，实时系统的测试等。在图5中给出SIP代理模式的消息顺序图。在代理模式下，UA1向PS发出会话邀请INVITE，PS通过Henning命令向LS查询UA2的信息，LS把UA2的信息回送给PS，PS向UA2转发UA1的会话请求INVITE，假定UA2回送确认连接信息200 OK给PS，则PS把向UA发送确认连接信息200 OK，UA1直接给UA2发送确认信息ACK，此时，连接建立，开始会话，当一方请求终止会话时，假定UA1请求终止会话，则UA1向PS发送终止信息BYE，PS把次信息转发给UA2，用户代理2向PS发送确认信息OK，PS把确认信息转发给UA1，会话终止。 3 结语在SIP系统模型的形式化描述中，重点描述了系统级和功能级的形式化，给出了更详尽的方案并验证了它的可行性和可靠性。在总体上分析了SIP系统的主要组成，用SDL语言和MSC语言形式化地描述了SIP协议的主要系统模型。通过利用SDL语言定义系统进程行为的内在行为及状态机来形式化描述SIP协议的主要组件，SDL语言和MSC语言的组合提供了一种有效的方法去验证SIP系统模型的描述。然后采用交互式的MSC图验证形式化模型的正确性。通过对SIP协议系统模型的形式化描述，对于以后SIP协议系统的开发提供了形式化的方法，也为开发其他通信协议形式化描述提供了借鉴，对于用形式化方法研究通信协议并开发通信协议可重用部件库具有实际意义。