計(jì)算機(jī)網(wǎng)絡(luò)多樣化的發(fā)展催生出大量新的路由協(xié)議,這些路由協(xié)議的安全性和正確性問題亟待解決。目前,基于形式化的方法、技術(shù)、工具已大量應(yīng)用在路由協(xié)議研究上,幫助實(shí)現(xiàn)協(xié)議的設(shè)計(jì)和實(shí)施。但現(xiàn)實(shí)問題是,一方面路由協(xié)議的發(fā)展變得多樣化,協(xié)議應(yīng)用的網(wǎng)絡(luò)規(guī)模從少節(jié)點(diǎn)到多節(jié)點(diǎn)不等;分層路由和人為規(guī)定的選路策略也使得概念簡(jiǎn)單清晰、性能優(yōu)良的算法變得復(fù)雜;通信鏈路和節(jié)點(diǎn)的不可靠使網(wǎng)絡(luò)拓?fù)涑蕜?dòng)態(tài)變化。另一方面,形式化方法的理論較深,規(guī)約、建模語言多樣,模型檢驗(yàn)、定理證明技術(shù)多樣,支持形式化驗(yàn)證的工具多樣。相比理論上的可行性,形式化方法的工具仍然較弱。因此,網(wǎng)絡(luò)協(xié)議研究人員如果想掌握全部知識(shí)似乎不可行,選擇合適的形式化驗(yàn)證方法、技術(shù)、工具應(yīng)用在路由協(xié)議設(shè)計(jì)和實(shí)現(xiàn)上,也需要花費(fèi)大量時(shí)間和精力。本文提出一種基于模型檢驗(yàn)的路由協(xié)議正確性和安全性的驗(yàn)證方法,該方法通過對(duì)協(xié)議的假設(shè)和簡(jiǎn)化抽取出模型,并通過基于反例的抽象精化技術(shù)實(shí)行驗(yàn)證和模型精化。將該方法應(yīng)用在三個(gè)路由協(xié)議的建模和驗(yàn)證上,使用有代表性的模型檢驗(yàn)工具SPIN和CBMC驗(yàn)證了包括安全性、正確性和收斂性的性質(zhì),通過對(duì)驗(yàn)證結(jié)果的分析,有效說明了該方法的可行性。 

【文章來源】：南京航空航天大學(xué)江蘇省 211工程院校

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

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

【文章目錄】：
摘要
ABSTRACT
注釋表
第一章 緒論
    1.1 課題研究背景
    1.2 國(guó)內(nèi)外研究現(xiàn)狀
    1.3 論文的選題依據(jù)和內(nèi)容
    1.4 論文的結(jié)構(gòu)安排
第二章 模型檢驗(yàn)及工具綜述
    2.1 模型檢驗(yàn)概述
        2.1.1 顯式模型檢驗(yàn)
        2.1.2 符號(hào)模型檢驗(yàn)
        2.1.3 有界模型檢驗(yàn)
        2.1.4 抽象技術(shù)
    2.2 模型檢驗(yàn)工具SPIN
        2.2.1 建模語言Promela
        2.2.2 性質(zhì)描述-線性時(shí)序邏輯
        2.2.3 使用SPIN驗(yàn)證
    2.3 模型檢驗(yàn)工具CBMC
        2.3.1 CBMC建模程序內(nèi)部變換特點(diǎn)
        2.3.2 性質(zhì)描述
        2.3.3 使用CBMC驗(yàn)證
    2.4 本章小結(jié)
第三章 使用模型檢驗(yàn)驗(yàn)證路由協(xié)議的方法
    3.1 路由協(xié)議化簡(jiǎn)的基本原則
        3.1.1 路由協(xié)議簡(jiǎn)述
        3.1.2 化簡(jiǎn)原則
    3.2 基于模型檢驗(yàn)的路由協(xié)議建模和驗(yàn)證
    3.3 本章小結(jié)
第四章 使用模型檢驗(yàn)驗(yàn)證路由協(xié)議的實(shí)例分析
    4.1 實(shí)例之OSPF
        4.1.1 OSPF基礎(chǔ)
        4.1.2 OSPF建模
        4.1.3 OSPF安全性描述
    4.2 實(shí)例之Chord
        4.2.1 Chord基礎(chǔ)
        4.2.2 Chord建模
        4.2.3 Chord正確性描述
    4.3 實(shí)例之BGP
        4.3.1 BGP基礎(chǔ)
        4.3.2 BGP建模
        4.3.3 BGP收斂性描述
    4.4 本章小結(jié)
第五章 實(shí)驗(yàn)結(jié)果與分析
    5.1 實(shí)驗(yàn)結(jié)果
        5.1.1 OSPF驗(yàn)證結(jié)果
        5.1.2 Chord驗(yàn)證結(jié)果
        5.1.3 BGP驗(yàn)證結(jié)果
    5.2 SPIN與CBMC在路由協(xié)議驗(yàn)證上的性能對(duì)比
    5.3 本章小結(jié)
第六章 總結(jié)與展望
    6.1 論文總結(jié)
    6.2 未來工作展望
參考文獻(xiàn)
致謝
在學(xué)期間的研究成果及發(fā)表的學(xué)術(shù)論文


【參考文獻(xiàn)】：
期刊論文
[1]模型檢測(cè)中狀態(tài)爆炸問題研究綜述[J]. 侯剛,周寬久,勇嘉偉,任龍濤,王小龍.  計(jì)算機(jī)科學(xué). 2013(S1)
[2]安全協(xié)議20年研究進(jìn)展[J]. 卿斯?jié)h.  軟件學(xué)報(bào). 2003(10)



本文編號(hào)：3062838