HMIPv6協(xié)議形式化建模及測試例生成方法研究.pdf

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

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

3、描述具有這些特點的系統(tǒng)。CPN tools還支持模型相關(guān)性質(zhì)的分析，從而保證了模型的正確性。
　　 在一致性測試方法上，本文提出了由協(xié)議屬性指導的測試例生成。文中對屬性也采用Coloured Petri Nets進行形式化描述，給出了基于屬性的測試例生成算法。該算法使得測試例的生成過程簡單，直接，且針對性強。算法的提出使得測試例自動生成成為可能，本文作者開發(fā)了基于CPNs的測試例生成工具，重點實現(xiàn)了本文提出的屬性指導的測試例生成