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

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

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

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