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

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

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

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

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