分层TCPN模型下SIP协议的分析

马晓娟　宋金平

摘要：在《电脑知识与技术》2016年9月刊《SIP协议的分层TCPN建模》一文中，作者论述了SIP协议的分层TCPN建模，本文结合若干模型分析技术验证了此协议的正确性。经分析，指出可能出现死锁，并分析了死锁原因。最后针对协议的设计又提出了相应的优化措施。

关键词：验证；触发；死锁；优化

1概述

基于《SIP协议的分层TCPN建模》中所建立的SIP协议，本文首先验证了此模型能否满足协议里对时间的条件约束，而后结合路径分析状态空间分析、模型模拟等技术，对此模型能否达到协议功能进行了检验，并提出设计中可能进入死锁这一不足。

2分层TCPN模型下SIP协议的验证

2.1验证时间约束条件

因TCPN建模下定时规律是时间约束的重要体现，为保障模型对SIP协议的正确模拟，必需对其准确性做验证。下文以模型中UAC端定时器A与定时器B为例，阐述通过模型模拟方式验证定时规律的过程。触发定时器6次后，T1时间（往返时延）之后若还未接收到应答，定时器B就会被触发，也就是说Calling状态下的UAC，定时器A最多被触发6次，定时器B最多被触发1次。

为查看模型模拟的执行结果，需要设定精确的触发定时器的时间值予以比对。如果所设比对值与实际执行结果相同，表明对此定时器的定时规律建模正确。为精确描述两定时器的触发时机，首先将T1的初始值设为5（发出INVITE请求T1时间后，定时器A第1次被触发），协议执行时间设为0；0时刻发送INVITE请求，定时器A第一次被触发的时间是5，第二次被触发的时间是2*T1+5，即15，第三次被触发的时间是4*T1+15，即35，第四次被触发的时间是8*T1+35，即75，第五次被触发的时间是16*T1+75，即155，第六次被触发的时间是32*T1+155，即315，这样定时器B被触发的时间為315+T1，即320。如此即得出触发时间序列为5，15，35，75，155，315，320，将此序列看作参照值和实际模型模拟结果做比对。

在《SIP协议的分层TCPN建模》中所建的模型中定时器触发次数随机，定时器A触发次数是[0，6]间随机整数。假设定时器A触发次数为m（0

如表1所示，使得两个SUCCESS函数维持假值不变。对于变迁TransErr而言，导致TransErr始终都不发生，从而可避免因发生传输层错误引起的协议状态转移，进而无从验证仅在Calling状态下才有效的两定时器的定时规律。对于变迁CTOS而言，导致CTOS始终不会触发，等效于模拟出一条0可靠率的链路，从而不断激活定时器的超时事件，这有助于我们验证定时器的触发规律。

调整参数后，模拟模型的运行结果截图如图1所示。图中库所CollectorCTS附近的几个值体现了每个消息被触发的时间，INVITE@O意为在初始状态下UAC发送出去的INVITE请求，余下的INVITE均由定时器A所触发。因定时器A控制重传消息，故其触发时间可由重传消息所附带的时间值进行提取。而触发定时器B可转移UAC状态，故其触发时间可由用以描述UAC状态的库所Scenec进行提取。由图l可知两定时器的触发规律与本文前面所提到的比对值一致，从而对定时器建模是否正确做出了验证。

2.2验证协议的正确性

下文采用状态空间分析技术，从模型是否存在死变迁、活锁和死锁这三个角度对协议进行更深入的验证。死变迁即模型中从来没有被点火的变迁，说明模型建模时存在冗余。活锁指的是环状状态空间，一旦进人就不能离开，如此循环往复。对SIP的INVlTE而言，正常终结状态是UAS与UAC均处于终结状态，若与此不符则陷入死锁。

表2是TCPN模型下SIP协议的状态空间分析结果，表中反映出状态空间和与之对应的强连通图所含的弧与节点数等值，说明不可靠链路下的INVITE事务不存在活锁，也不存在死变迁和活变迁。