隨著網(wǎng)絡(luò)信息化的快速發(fā)展,可靠的網(wǎng)絡(luò)協(xié)議成為保障網(wǎng)絡(luò)穩(wěn)定的重要因素。對網(wǎng)絡(luò)協(xié)議進(jìn)行驗(yàn)證不僅可以最大限度地檢測和糾正協(xié)議開發(fā)前期的錯誤和缺陷,還可以對已設(shè)計的協(xié)議進(jìn)行分析和驗(yàn)證,找出其中潛在的錯誤。形式化地描述和驗(yàn)證協(xié)議是整個協(xié)議設(shè)計與實(shí)現(xiàn)的基礎(chǔ),對協(xié)議實(shí)現(xiàn)的正確性、完整性和復(fù)雜度有重要的影響。形式化的建模工具CPN不但可以提高網(wǎng)絡(luò)協(xié)議驗(yàn)證的自動化程度,而且有效的保證了協(xié)議自身的正確性和無歧義性。IS-IS路由協(xié)議作為當(dāng)前內(nèi)部網(wǎng)關(guān)的主流協(xié)議之一,采用分層的網(wǎng)絡(luò)結(jié)構(gòu),穩(wěn)定性好、收斂快等優(yōu)點(diǎn)使得IS-IS路由協(xié)議在網(wǎng)絡(luò)中得到了廣泛的應(yīng)用。但到現(xiàn)在為止還沒有關(guān)于IS-IS路由協(xié)議進(jìn)行驗(yàn)證的文獻(xiàn),所以本文進(jìn)行了基于CPN的IS-IS路由協(xié)議驗(yàn)證。本文首先通過對IS-IS路由協(xié)議的仔細(xì)研究,對IS-IS路由協(xié)議層次化結(jié)構(gòu)-子網(wǎng)相關(guān)功能和子網(wǎng)獨(dú)立功能模塊分別進(jìn)行了CPN建模；然后通過CPN建模工具的模擬執(zhí)行和狀態(tài)空間技術(shù)從整體上對IS-IS路由協(xié)議的正確性進(jìn)行了驗(yàn)證；最后對IS-IS路由協(xié)議的協(xié)議屬性DIS選舉、LSP/CSNP引發(fā)決定進(jìn)程和最短路徑的更新進(jìn)行了性能驗(yàn)證,從驗(yàn)證結(jié)果可以看出IS-IS... 

【文章來源】：內(nèi)蒙古大學(xué)內(nèi)蒙古自治區(qū) 211工程院校

【文章頁數(shù)】：60 頁

【學(xué)位級別】：碩士

【文章目錄】：
摘要
ABSTRACT
目錄
圖表目錄
第一章 引言
    1.1 研究背景及意義
    1.2 研究內(nèi)容和主要工作
    1.3 論文結(jié)構(gòu)
第二章 背景知識介紹
    2.1 IS-IS協(xié)議簡介
    2.2 CPN簡介
    2.3 CPN Tools 簡介
    2.4 協(xié)議驗(yàn)證簡介
    2.5 本章小結(jié)
第三章 IS-IS協(xié)議的分析
    3.1 IS-IS路由協(xié)議數(shù)據(jù)的類型和建模的數(shù)據(jù)類型
    3.2 IS-IS 路由協(xié)議數(shù)據(jù)的結(jié)構(gòu)和建模中數(shù)據(jù)包的結(jié)構(gòu)
    3.3 IS-IS 路由協(xié)議功能
        3.3.1 子網(wǎng)相關(guān)功能
        3.3.2 子網(wǎng)獨(dú)立功能
    3.4 本章小結(jié)
第四章 IS-IS路由協(xié)議的形式化建模
    4.1 CPN模型的抽象
    4.2 數(shù)據(jù)建模
    4.3 CPN層次化建模
        4.3.1 TOP層模型
        4.3.2 子網(wǎng)相關(guān)功能接收子模塊
        4.3.3 子網(wǎng)獨(dú)立功能的接收進(jìn)程模塊
        4.3.4 子網(wǎng)獨(dú)立功能的更新進(jìn)程模塊
        4.3.5 子網(wǎng)獨(dú)立功能的決定進(jìn)程模塊
        4.3.6 子網(wǎng)獨(dú)立功能的轉(zhuǎn)發(fā)進(jìn)程模塊
        4.3.7 子網(wǎng)相關(guān)功能的發(fā)送進(jìn)程模塊
    4.4 本章小結(jié)
第五章 IS-IS路由協(xié)議模型驗(yàn)證與分析
    5.1 IS-IS路由協(xié)議正確性的驗(yàn)證
    5.2 協(xié)議屬性的驗(yàn)證
        5.2.1 DIS屬性驗(yàn)證
        5.2.2 LSP/CSNP信息引發(fā)決定進(jìn)程屬性驗(yàn)證
        5.2.3 最短路徑的更新屬性驗(yàn)證
    5.3 本章小結(jié)
第六章 總結(jié)和展望
    6.1 總結(jié)
    6.2 未來研究方向的展望
參考文獻(xiàn)
致謝


【參考文獻(xiàn)】：
期刊論文
[1]Sip協(xié)議的petri網(wǎng)建模及性能驗(yàn)證[J]. 楊郁州,張偉,占東生.  微計算機(jī)信息. 2010(21)
[2]基于CPN TOOLS的網(wǎng)絡(luò)協(xié)議建模與仿真技術(shù)研究[J]. 占東生,張偉,顧明甲.  微計算機(jī)信息. 2010(13)
[3]基于層次結(jié)構(gòu)的IS-IS協(xié)議一致性測試[J]. 康鑫,周顥,趙保華.  計算機(jī)工程. 2007(18)
[4]集成IS-IS路由選擇協(xié)議的研究[J]. 康京山,韓春剛.  無線電通信技術(shù). 2007(02)
[5]基于著色petri網(wǎng)的安全協(xié)議驗(yàn)證方法[J]. 劉進(jìn),陳丹,肖德寶.  華中師范大學(xué)學(xué)報(自然科學(xué)版). 2006(03)
[6]IS-IS路由協(xié)議一致性測試的研究與實(shí)現(xiàn)[J]. 范煒瑋,蘇金樹,彭偉.  計算機(jī)工程與科學(xué). 2006(07)
[7]OSPF和集成IS-IS路由協(xié)議的深入研究[J]. 張浩鋒.  廣東通信技術(shù). 2004(12)
[8]大型IP網(wǎng)絡(luò)IS-IS路由規(guī)劃與設(shè)計[J]. 王香剛.  深圳信息職業(yè)技術(shù)學(xué)院學(xué)報. 2004(01)
[9]網(wǎng)絡(luò)協(xié)議描述和驗(yàn)證技術(shù)的分析與比較[J]. 冷淑霞,徐濤.  山東理工大學(xué)學(xué)報(自然科學(xué)版). 2004(02)

碩士論文
[1]基于時間著色Petri網(wǎng)的SIP協(xié)議形式化驗(yàn)證與分析[D]. 馬元飛.內(nèi)蒙古大學(xué) 2012
[2]基于CPN的BitTorrent協(xié)議激勵機(jī)制研究[D]. 馬燕林.內(nèi)蒙古大學(xué) 2012
[3]協(xié)議可擴(kuò)展屬性測試方法的研究與實(shí)現(xiàn)[D]. 郭亞杰.內(nèi)蒙古大學(xué) 2012
[4]基于IS-IS路由協(xié)議的數(shù)據(jù)通信網(wǎng)絡(luò)拓?fù)浒l(fā)現(xiàn)方法的設(shè)計與實(shí)現(xiàn)[D]. 馬俐敏.北京郵電大學(xué) 2011
[5]基于著色Petri網(wǎng)的LDP協(xié)議驗(yàn)證研究[D]. 薩仁高娃.內(nèi)蒙古大學(xué) 2010
[6]IS-IS路由協(xié)議一致性測試的研究[D]. 劉瑩澤.內(nèi)蒙古大學(xué) 2008
[7]IS-IS路由性能監(jiān)測系統(tǒng)設(shè)計與實(shí)現(xiàn)[D]. 王衛(wèi)華.北京郵電大學(xué) 2008
[8]集成IS-IS協(xié)議在T比特路由器中研究與實(shí)現(xiàn)[D]. 周建林.中國人民解放軍信息工程大學(xué) 2005
[9]IS-IS協(xié)議路由計算方法的研究和實(shí)現(xiàn)[D]. 范煒瑋.國防科學(xué)技術(shù)大學(xué) 2004
[10]中間系統(tǒng)—中間系統(tǒng)路由協(xié)議IS-IS的研究與實(shí)現(xiàn)[D]. 梁暾.國防科學(xué)技術(shù)大學(xué) 2004



本文編號：3200763