基于正確性驗(yàn)證的SDH協(xié)議測(cè)試.pdf

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

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

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