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

1、近年來(lái)，關(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è)計(jì)上具有自身特殊的復(fù)雜性，在設(shè)計(jì)過程中經(jīng)常會(huì)出現(xiàn)一些人工方法難以察覺的缺陷。
　　模型檢測(cè)是一種形式化的驗(yàn)證技術(shù)，能夠?qū)ο到y(tǒng)進(jìn)行自動(dòng)驗(yàn)證，并在發(fā)現(xiàn)系統(tǒng)缺陷時(shí)，給出導(dǎo)致此缺陷出現(xiàn)的執(zhí)行路徑。借助模型檢測(cè)的這種特性可以發(fā)現(xiàn)路由協(xié)議中隱含的缺陷，從而提高路由協(xié)議的可靠

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

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