分層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事務不存在活鎖，也不存在死變遷和活變遷。