马晓娟　宋金平

摘要：在《电脑知识与技术》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，第二次被触发的时间是……