IPv6鄰居發(fā)現(xiàn)協(xié)議的形式化驗(yàn)證.pdf

1、隨著網(wǎng)絡(luò)和通信技術(shù)的高速發(fā)展,大量新的協(xié)議不斷被提出.但是,到目前為止,Internet的協(xié)議標(biāo)準(zhǔn)RFC仍然使用自然語言描述,Internet的協(xié)議實(shí)現(xiàn)也主要是采用人工編制完成,這種協(xié)議軟件開發(fā)是隨意的,并逐步擴(kuò)大的.隨著網(wǎng)絡(luò)服務(wù)要求的提高,網(wǎng)絡(luò)系統(tǒng)的復(fù)雜性在協(xié)議方面體現(xiàn)出空間分布性、并發(fā)性、異步性、不穩(wěn)定性和多樣性,網(wǎng)絡(luò)協(xié)議再也不可能用工程直覺方法設(shè)計(jì)出高質(zhì)量的協(xié)議,協(xié)議的完整性、正確性、安全性、可移植性和標(biāo)準(zhǔn)化都難以得到保證,而且協(xié)

2、議實(shí)現(xiàn)后糾正協(xié)議描述錯(cuò)誤的代價(jià)是十分可觀的.錯(cuò)誤或不完全的協(xié)議可能導(dǎo)致整個(gè)網(wǎng)絡(luò)的癱瘓,以及服務(wù)可靠性的降低.這就要求我們必須在協(xié)議投入實(shí)際應(yīng)用之前,進(jìn)行協(xié)議驗(yàn)證,來保證協(xié)議設(shè)計(jì)的正確性和完整性.也就是說,為了更好地研究和實(shí)現(xiàn)協(xié)議,應(yīng)該采用協(xié)議工程的方法,通過適當(dāng)?shù)募夹g(shù)和計(jì)算機(jī)輔助工具,來設(shè)計(jì)和維護(hù)網(wǎng)絡(luò)協(xié)議.協(xié)議形式化理論是協(xié)議工程學(xué)的核心.形式化驗(yàn)證技術(shù)在協(xié)議的驗(yàn)證工作中,具有良好的發(fā)展前途,并且近幾年來受到了廣泛的重視.形式化說明語言