馬曉娟　宋金平

摘要：在《電腦知識與技術(shù)》2016年9月刊《SIP協(xié)議的分層TCPN建?！芬晃闹校髡哒撌隽薙IP協(xié)議的分層TCPN建模，本文結(jié)合若干模型分析技術(shù)驗證了此協(xié)議的正確性。經(jīng)分析，指出可能出現(xiàn)死鎖，并分析了死鎖原因。最后針對協(xié)議的設(shè)計又提出了相應(yīng)的優(yōu)化措施。

關(guān)鍵詞：驗證；觸發(fā)；死鎖；優(yōu)化

1概述

基于《SIP協(xié)議的分層TCPN建?！分兴⒌腟IP協(xié)議，本文首先驗證了此模型能否滿足協(xié)議里對時間的條件約束，而后結(jié)合路徑分析狀態(tài)空間分析、模型模擬等技術(shù)，對此模型能否達到協(xié)議功能進行了檢驗，并提出設(shè)計中可能進入死鎖這一不足。

2分層TCPN模型下SIP協(xié)議的驗證

2.1驗證時間約束條件

因TCPN建模下定時規(guī)律是時間約束的重要體現(xiàn)，為保障模型對SIP協(xié)議的正確模擬，必需對其準確性做驗證。下文以模型中UAC端定時器A與定時器B為例，闡述通過模型模擬方式驗證定時規(guī)律的過程。觸發(fā)定時器6次后，T1時間（往返時延）之后若還未接收到應(yīng)答，定時器B就會被觸發(fā)，也就是說Calling狀態(tài)下的UAC，定時器A最多被觸發(fā)6次，定時器B最多被觸發(fā)1次。

為查看模型模擬的執(zhí)行結(jié)果，需要設(shè)定精確的觸發(fā)定時器的時間值予以比對。如果所設(shè)比對值與實際執(zhí)行結(jié)果相同，表明對此定時器的定時規(guī)律建模正確。為精確描述兩定時器的觸發(fā)時機，首先將T1的初始值設(shè)為5（發(fā)出INVITE請求T1時間后，定時器A第1次被觸發(fā)），協(xié)議執(zhí)行時間設(shè)為0；0時刻發(fā)送INVITE請求，定時器A第一次被觸發(fā)的時間是5，第二次被觸發(fā)的時間是2*T1+5，即15，第三次被觸發(fā)的時間是4*T1+15，即35，第四次被觸發(fā)的時間是8*T1+35，即75，第五次被觸發(fā)的時間是16*T1+75，即155，第六次被觸發(fā)的時間是32*T1+155，即315，這樣定時器B被觸發(fā)的時間為315+T1，即320。如此即得出觸發(fā)時間序列為5，15，35，75，155，315，320，將此序列看作參照值和實際模型模擬結(jié)果做比對。

在《SIP協(xié)議的分層TCPN建?！分兴ǖ哪Ｐ椭卸〞r器觸發(fā)次數(shù)隨機，定時器A觸發(fā)次數(shù)是[0，6]間隨機整數(shù)。假設(shè)定時器A觸發(fā)次數(shù)為m（0

如表1所示，使得兩個SUCCESS函數(shù)維持假值不變。對于變遷TransErr而言，導致TransErr始終都不發(fā)生，從而可避免因發(fā)生傳輸層錯誤引起的協(xié)議狀態(tài)轉(zhuǎn)移，進而無從驗證僅在Calling狀態(tài)下才有效的兩定時器的定時規(guī)律。對于變遷CTOS而言，導致CTOS始終不會觸發(fā)，等效于模擬出一條0可靠率的鏈路，從而不斷激活定時器的超時事件，這有助于我們驗證定時器的觸發(fā)規(guī)律。

調(diào)整參數(shù)后，模擬模型的運行結(jié)果截圖如圖1所示。圖中庫所CollectorCTS附近的幾個值體現(xiàn)了每個消息被觸發(fā)的時間，INVITE@O意為在初始狀態(tài)下UAC發(fā)送出去的INVITE請求，余下的INVITE均由定時器A所觸發(fā)。因定時器A控制重傳消息，故其觸發(fā)時間可由重傳消息所附帶的時間值進行提取。而觸發(fā)定時器B可轉(zhuǎn)移UAC狀態(tài)，故其觸發(fā)時間可由用以描述UAC狀態(tài)的庫所Scenec進行提取。由圖l可知兩定時器的觸發(fā)規(guī)律與本文前面所提到的比對值一致，從而對定時器建模是否正確做出了驗證。

2.2驗證協(xié)議的正確性

下文采用狀態(tài)空間分析技術(shù)，從模型是否存在死變遷、活鎖和死鎖這三個角度對協(xié)議進行更深入的驗證。死變遷即模型中從來沒有被點火的變遷，說明模型建模時存在冗余?；铈i指的是環(huán)狀狀態(tài)空間，一旦進人就不能離開，如此循環(huán)往復。對SIP的INVlTE而言，正常終結(jié)狀態(tài)是UAS與UAC均處于終結(jié)狀態(tài)，若與此不符則陷入死鎖。

表2是TCPN模型下SIP協(xié)議的狀態(tài)空間分析結(jié)果，表中反映出狀態(tài)空間和與之對應(yīng)的強連通圖所含的弧與節(jié)點數(shù)等值，說明不可靠鏈路下的INVITE事務(wù)不存在活鎖，也不存在死變遷和活變遷。