基于Color Petri Nets的HMIPv6協(xié)議形式化驗(yàn)證研究.pdf

1、層次移動IPv6（Hierachical MobileIPv6，HMIPv6）是在MIPv6（移動IPv6）的基礎(chǔ)上針對MN（移動結(jié)點(diǎn)）在小范圍內(nèi)快速移動所作出的一種改進(jìn)技術(shù)。HMIPv6針對MIPv6將全局性的大范圍移動與一個區(qū)域內(nèi)的小范圍的移動都用一種方式處理，對移動結(jié)點(diǎn)MN在小范圍內(nèi)快速移動切換時更新報文頻繁問題提出了解決方法。HMIPv6對網(wǎng)絡(luò)進(jìn)行了層次化的劃分，HMIPv6在每個區(qū)域內(nèi)引入了一個新的實(shí)體--移動錨點(diǎn)（MAP），

2、使得移動結(jié)點(diǎn)的移動分為“宏移動”和“微移動”兩種情況，改進(jìn)了最基本的MIPv6切換方案，減少了移動過程中的丟包率和傳輸延時，提高了通信質(zhì)量。
　　 對HMIPv6進(jìn)行形式化驗(yàn)證不僅可以給出協(xié)議的一種形式化的規(guī)范描述，并且可以為后續(xù)協(xié)議改進(jìn)提供了基礎(chǔ)模型，便于協(xié)議改進(jìn)的分析，并為軟件的實(shí)現(xiàn)提供了可信性保障。本文采用“基于事件”的分析方法對HMIPv6協(xié)議進(jìn)行屬性提取，并采用了層次化方法和“通用模塊”思想，構(gòu)建了著色Petri網(wǎng)（C