OSPFv3協(xié)議的實(shí)踐與一致性測(cè)試生成.pdf

1、該文首先介紹了OSPF協(xié)議的背景和主要功能,重點(diǎn)總結(jié)了OSPFv3協(xié)議不同于OSPFv2協(xié)議的方面以及IPv6協(xié)議對(duì)OSPFv3協(xié)議的封裝.接著,該文介紹了協(xié)議測(cè)試的分類(lèi),協(xié)議一致性測(cè)試的概念以及測(cè)試過(guò)程要經(jīng)歷的四個(gè)階段.在介紹有關(guān)形式描述技術(shù)概念的同時(shí),簡(jiǎn)單地說(shuō)明了幾種形式描述技術(shù),并對(duì)它們的特點(diǎn)進(jìn)行了比較.在介紹SDL語(yǔ)言時(shí),對(duì)它的發(fā)展背景、適用范圍、語(yǔ)言特點(diǎn)、相應(yīng)的軟件工具等都做了詳細(xì)的介紹.對(duì)SDL語(yǔ)言的語(yǔ)法規(guī)則和結(jié)構(gòu),也通過(guò)文

2、字與圖形相結(jié)合的方法給出了說(shuō)明.另外,還簡(jiǎn)要介紹了另一種從SDL發(fā)展而來(lái)的建模語(yǔ)言MSC.該文中將用到這兩種建模語(yǔ)言為OSPF協(xié)議建立模型.然后,該文提出了一種為協(xié)議建模的方法.從協(xié)議的自然語(yǔ)言描述出發(fā),得到協(xié)議的有限狀態(tài)機(jī)描述;再將協(xié)議的有限狀態(tài)機(jī)描述通過(guò)該文提出的算法轉(zhuǎn)換成協(xié)議的SDL模型.在提出了從有限狀態(tài)機(jī)到SDL模型的轉(zhuǎn)換算法后,給出了描述協(xié)議進(jìn)程處理的SDL模型和描述協(xié)議數(shù)據(jù)處理的MSC模型.最后,該文提出了生成協(xié)議的一致性