SIP协议系统模型的形式化研究

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协议系统的开发提供了形式化的方法，也为开发其他通信协议形式化描述提供了借鉴，对于用形式化方法研究通信协议并开发通信协议可重用部件库具有实际意义。

作者：李中华，穆维新，刘润杰，申金媛　单位：郑州大学信息工程学院

来源：现代电子技术