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

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

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

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

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