基于時間著色Petri網(wǎng)的SIP協(xié)議形式化驗證與分析.pdf

1、隨著云計算和物聯(lián)網(wǎng)技術(shù)的興起，聯(lián)網(wǎng)設(shè)備逐漸向移動化、小型化、功能集成化發(fā)展，會話初始化協(xié)議(SessionInitiationProtocol，SIP)協(xié)議以其無縫、靈活、可擴展的特性順應(yīng)了技術(shù)發(fā)展的要求，在許多領(lǐng)域發(fā)揮著重要的作用，同時應(yīng)用領(lǐng)域也隨著下一代互聯(lián)網(wǎng)(NextGenerationNetwork，NGN)的發(fā)展而不斷擴大。為了適應(yīng)各種網(wǎng)絡(luò)環(huán)境及SIP應(yīng)用的需要，須對協(xié)議進(jìn)行必要的擴展、修改和進(jìn)一步完善。然而技術(shù)的發(fā)展使得網(wǎng)絡(luò)

2、協(xié)議的開發(fā)難度也進(jìn)一步加大，協(xié)議開發(fā)過程中任何一點錯誤和缺陷都將給系統(tǒng)的穩(wěn)定性、可靠性、安全性等帶來巨大的影響。如何較早的發(fā)現(xiàn)協(xié)議中存在問題，去除風(fēng)險，降低應(yīng)用開發(fā)和維護(hù)成本，是一個值得研究的課題。
　　 為了實現(xiàn)上述目的，采用形式化的方法對協(xié)議進(jìn)行建模以及分析，可以有效的保證協(xié)議自身的正確性，無歧義性。一個定義完備驗證無誤的協(xié)議可以有效的減少后期的開發(fā)以及維護(hù)費用。另外從協(xié)議工程的角度看，驗證也是一個協(xié)議開發(fā)生命周期中重要的步

3、驟。時間著色Petri網(wǎng)(TimedColoredPetriNet，TCPN)作為一種形式化建模與分析技術(shù)，非常適合描述具有并發(fā)行為及時間約束條件的通信系統(tǒng)。目前對SIP的研究很多，但缺少對SIP的形式化驗證和模型分析，不能反映出SIP整體的特性，基于層次TCPN對SIP協(xié)議進(jìn)行建模與驗證更是不多見。
　　 本文針對這些方面研究的不足，提出了一種基于TCPN的SIP協(xié)議狀態(tài)分層建模方法，指導(dǎo)在不同狀態(tài)下對協(xié)議功能行為進(jìn)行分層抽象

4、建模。并在該方法的指導(dǎo)下，給出了該協(xié)議的層次TCPN模型，準(zhǔn)確、直觀的描述了協(xié)議的主體功能行為。之后，對SIP中的時間約束條件進(jìn)行了驗證，使模型按照協(xié)議約束的特定時間進(jìn)行狀態(tài)轉(zhuǎn)移與消息交互，保證了模型對協(xié)議時間細(xì)節(jié)的精確刻畫。然后，在系統(tǒng)TCPN模型的基礎(chǔ)上，集成模擬、狀態(tài)空間分析和模型檢驗等技術(shù)，在協(xié)議模型的不同抽象層次上完成協(xié)議分析，驗證模型滿足協(xié)議需求的部分。最后，通過正則表達(dá)式完成對模型模擬生成數(shù)據(jù)的采集過濾，并對協(xié)議進(jìn)行路徑分