基于正確性驗證的SDH協(xié)議測試.pdf

1、SDH協(xié)議在現(xiàn)代信息傳輸中顯露出了強大的生命力.SDH收/發(fā)器是用于SDH光網(wǎng)絡(luò)的重要器件,是SDH的協(xié)議實現(xiàn).為了對SDH協(xié)議進行更徹底、更正確、更全面的測試,本文將在對SDH形式化模型進行正確性驗證的基礎(chǔ)上,利用開發(fā)的測試系統(tǒng)工具對邏輯仿真的SDH收/發(fā)器進行測試,最終完成對SDH協(xié)議的測試工作.形式化模型采用了直觀高效的EFSM模型和Petri網(wǎng)模型,并以這兩種模型為例,提出了基于模型轉(zhuǎn)換的正確性驗證方法,對SDH形式化模型進行了

2、驗證,隨后依據(jù)一致性測試理論,本文提供了采用UIO方法生成SDH測試序列的途徑,并為補充測試序列完備性增加了相應(yīng)的測試用例.利用TCL/TK開發(fā)的SDH測試系統(tǒng)采用管道-過濾器技術(shù)設(shè)計,并使用緩沖區(qū)管理機制對管道進行了擴展;同時系統(tǒng)平臺還提供了TCL擴展接口,測試者可以通過測控軟件的人機交互接口直接對SDH測試過程進行動態(tài)控制.對SDH協(xié)議進行形式化建模,是貫穿此項協(xié)議工程始末的核心技術(shù),對SDH形式化模型進行正確性驗證,是進行協(xié)議測試

3、的保障,我們開發(fā)的SDH測試系統(tǒng),又為SDH這種新型的傳輸機制提供了一個有效的測試工具.基于正確性驗證的SDH協(xié)議測試,從理論的高度為協(xié)議測試拓展了一條新穎的思路,而后續(xù)開展的測試實踐又直觀地展示了此項研究最終能達到的效果.本文主要完成了利用EFSM模型以及Petri網(wǎng)模型為SDH協(xié)議進行形式化建模的示例;隨后研究模型間相互轉(zhuǎn)換的理論,提出了基于模型互換的正確性驗證方法,并利用此法對SDH的形式化描述進行了驗證;在正確性驗證的保證下,分