HMIPv6協(xié)議形式化建模及測(cè)試?yán)煞椒ㄑ芯?pdf

1、隨著網(wǎng)絡(luò)通信技術(shù)的高速發(fā)展，網(wǎng)絡(luò)協(xié)議標(biāo)準(zhǔn)也不斷地更新和完善。如何更有效地保證網(wǎng)絡(luò)協(xié)議的實(shí)現(xiàn)質(zhì)量，已成為網(wǎng)絡(luò)協(xié)議工程領(lǐng)域的關(guān)鍵問(wèn)題之一。實(shí)踐證明，以合理有效的方式將形式化方法應(yīng)用于協(xié)議研發(fā)實(shí)踐中，可以有效提高協(xié)議設(shè)計(jì)、實(shí)現(xiàn)、測(cè)試的效率，最大程度地保證協(xié)議實(shí)現(xiàn)的正確性。協(xié)議一致性測(cè)試用于檢查協(xié)議賣現(xiàn)是否符合協(xié)議設(shè)計(jì)的要求，是保障協(xié)議實(shí)現(xiàn)質(zhì)量的有效方法。
　　 HMIPv6協(xié)議作為移動(dòng)IPv6協(xié)議的優(yōu)化，在行為特性、安全性等方面采用了

2、新的技術(shù)。如何借助于形式化方法對(duì)此協(xié)議進(jìn)行有效的一致性測(cè)試成為亟待解決的問(wèn)題。
　　 本文采用Coloured Petri Nets對(duì)HMIPv6協(xié)議進(jìn)行形式化建模，并且使用了層次化的建模方法，將HMIPv6協(xié)議按節(jié)點(diǎn)類型抽象成若干層，層次化的模型不但更能體現(xiàn)不同節(jié)點(diǎn)間的交互屬性，而且由于層次間的相對(duì)獨(dú)立性，使得模型的開(kāi)發(fā)更加模塊化。此類通信協(xié)議的特點(diǎn)是并發(fā)度較高，且交互行為較多，Coloured Petri Nets非常適合于

3、描述具有這些特點(diǎn)的系統(tǒng)。CPN tools還支持模型相關(guān)性質(zhì)的分析，從而保證了模型的正確性。
　　 在一致性測(cè)試方法上，本文提出了由協(xié)議屬性指導(dǎo)的測(cè)試?yán)伞Ｎ闹袑?duì)屬性也采用Coloured Petri Nets進(jìn)行形式化描述，給出了基于屬性的測(cè)試?yán)伤惴āＴ撍惴ㄊ沟脺y(cè)試?yán)纳蛇^(guò)程簡(jiǎn)單，直接，且針對(duì)性強(qiáng)。算法的提出使得測(cè)試?yán)詣?dòng)生成成為可能，本文作者開(kāi)發(fā)了基于CPNs的測(cè)試?yán)晒ぞ?，重點(diǎn)實(shí)現(xiàn)了本文提出的屬性指導(dǎo)的測(cè)試?yán)?/p>