基于著色Petri網(wǎng)的LDP協(xié)議驗(yàn)證研究.pdf

1、網(wǎng)絡(luò)協(xié)議具有空間分布性、并發(fā)性和異步性，這些特性對(duì)網(wǎng)絡(luò)協(xié)議的開發(fā)質(zhì)量帶來了巨大挑戰(zhàn)。協(xié)議的驗(yàn)證是對(duì)協(xié)議的功能和性能進(jìn)行校驗(yàn)過程，是保證協(xié)議開發(fā)質(zhì)量的必要環(huán)節(jié)。協(xié)議形式化驗(yàn)證的前提是協(xié)議行為以及協(xié)議性質(zhì)的形式描述。協(xié)議的行為可通過形式模型或者形式語言進(jìn)行描述，而協(xié)議性質(zhì)的描述方式是系統(tǒng)斷言語言，如CTL、ASK-CTL等。模型檢查作為一種形式化驗(yàn)證方法，能夠自動(dòng)驗(yàn)證一個(gè)系統(tǒng)是否滿足設(shè)計(jì)規(guī)范，近年來被廣泛應(yīng)用于軟硬件、協(xié)議驗(yàn)證中。通過協(xié)議模

2、型，可以從整體上、宏觀上把握協(xié)議，更早的發(fā)現(xiàn)問題或疏漏的地方。而且協(xié)議模型為協(xié)議實(shí)現(xiàn)代碼生成提供依據(jù)，允許詳細(xì)說明協(xié)議的結(jié)構(gòu)或行為，給出了一個(gè)指導(dǎo)構(gòu)造協(xié)議實(shí)現(xiàn)系統(tǒng)的模板。
　　 MPLS（MultiRotocol Label Switching，多協(xié)議標(biāo)記交換）技術(shù)是隨著Internet的發(fā)展而涌現(xiàn)出來的網(wǎng)絡(luò)新技術(shù)中的一種。MPLS利用簡單的定長的標(biāo)記來轉(zhuǎn)發(fā)分組，將傳統(tǒng)網(wǎng)絡(luò)層中復(fù)雜、靈活的路由協(xié)議與數(shù)據(jù)鏈路層便宜高速的交換硬件很

3、好地結(jié)合起來。LDP（Label Distribution Protocol，標(biāo)記分發(fā)協(xié)議）是為標(biāo)記分發(fā)而專門制定的新協(xié)議，使用LDP可以實(shí)現(xiàn)MPLS中標(biāo)記分發(fā)功能。
　　 論文首先使用CPN Tools工具設(shè)計(jì)和實(shí)現(xiàn)了LDP協(xié)議特定模式下的CPN（Colored Petri Net，著色Petri網(wǎng)）模型。然后使用CPN Tools的狀態(tài)空間工具模擬得到了協(xié)議分析報(bào)告。最后在協(xié)議分析報(bào)告的基礎(chǔ)上結(jié)合使用分支時(shí)序邏輯ASK-CT