基于UPPAAL的路由協(xié)議驗證.pdf

1、近年來，關(guān)于下一代互聯(lián)網(wǎng)和物聯(lián)網(wǎng)的研究成果日漸豐富，新的數(shù)據(jù)通信和傳輸方法不斷涌現(xiàn)。其中，新的路由協(xié)議是新型網(wǎng)絡(luò)的關(guān)鍵部分，其正確性直接影響著網(wǎng)絡(luò)的穩(wěn)定性。然而路由協(xié)議在設(shè)計上具有自身特殊的復(fù)雜性，在設(shè)計過程中經(jīng)常會出現(xiàn)一些人工方法難以察覺的缺陷。
　　模型檢測是一種形式化的驗證技術(shù)，能夠?qū)ο到y(tǒng)進行自動驗證，并在發(fā)現(xiàn)系統(tǒng)缺陷時，給出導(dǎo)致此缺陷出現(xiàn)的執(zhí)行路徑。借助模型檢測的這種特性可以發(fā)現(xiàn)路由協(xié)議中隱含的缺陷，從而提高路由協(xié)議的可靠

2、性。基于時間自動機的模型檢測工具UPPAAL是一個高效的可達性分析工具，常常被應(yīng)用于包括網(wǎng)絡(luò)協(xié)議在內(nèi)的各類實時系統(tǒng)的驗證。然而，使用模型檢測方法對路由協(xié)議進行驗證時，還存在以下兩方面的問題，一方面是協(xié)議建模困難，其中的關(guān)鍵在于復(fù)雜定時數(shù)據(jù)的建模;另一方面是狀態(tài)爆炸問題嚴重。
　　本文首先對路由協(xié)議中存在的復(fù)雜定時數(shù)據(jù)進行研究。針對復(fù)雜定時數(shù)據(jù)建模困難的問題，提出了一種基于離散化的抽象建模方法。通過實驗測試了這種建模方法的有效性，并

3、通過進一步實驗分析了這種建模方法的性能。
　　針對模型檢測的狀態(tài)爆炸問題，本文在建模過程中采用抽象技術(shù)與組合技術(shù)把原模型分解為兩個子模型，分別對其進行驗證，并通過假設(shè)/保證的組合策略驗證了原模型的性質(zhì)。
　　最后，在抽象與組合技術(shù)以及復(fù)雜定時數(shù)據(jù)建模方法的基礎(chǔ)上，對OLSR路由協(xié)議進行驗證。實驗結(jié)果表明，0LSR協(xié)議具有無死鎖、行為一致性以及連通性。實驗結(jié)果同時表明，OLSR協(xié)議中的路由表計算部分存在冗余計算，可通過延遲路由