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

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

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