基于擴(kuò)展時(shí)間Petri網(wǎng)的協(xié)議描述與驗(yàn)證研究.pdf

1、協(xié)議是計(jì)算機(jī)網(wǎng)絡(luò)的命脈,協(xié)議復(fù)雜性的提高導(dǎo)致協(xié)議工程學(xué)科的出現(xiàn).協(xié)議工程的主要活動(dòng)包括協(xié)議描述、驗(yàn)證、性能分析、自動(dòng)實(shí)現(xiàn)和一致性測(cè)試,其中協(xié)議描述和分析是整個(gè)協(xié)議工程中最重要的活動(dòng)環(huán)節(jié),是協(xié)議工程其它活動(dòng)的基礎(chǔ).論文在總結(jié)比較現(xiàn)有的各種形式描述技術(shù)(FDT)的基礎(chǔ)之上,重點(diǎn)論述了采用Petri網(wǎng)作為協(xié)議描述和分析工具的優(yōu)勢(shì)所在.為了更好的擴(kuò)展時(shí)間Petri網(wǎng)的模擬能力以及建模的方便,在Merlin定義的時(shí)間Petri網(wǎng)的基礎(chǔ)之上添加了抑

2、止弧以實(shí)現(xiàn)對(duì)變遷激發(fā)的另一種控制,提出了帶抑止弧的時(shí)間Petri網(wǎng)系統(tǒng)(ETPN),并定義了ETPN網(wǎng)系統(tǒng)的狀態(tài)、變遷激發(fā)的條件和變遷激發(fā)的規(guī)則.在對(duì)該網(wǎng)系統(tǒng)進(jìn)行分析的基礎(chǔ)之上,發(fā)展了傳統(tǒng)的可達(dá)分析技術(shù).應(yīng)用帶抑止弧的時(shí)間Petri網(wǎng)對(duì)IEEE802.2 LLC3型協(xié)議進(jìn)行了建模.根據(jù)該文提出的可達(dá)分析技術(shù),推導(dǎo)出了保證協(xié)議正確操作的參數(shù)間的時(shí)間關(guān)系,根據(jù)該時(shí)間關(guān)系,我們得到了所建模型的簡(jiǎn)化的可達(dá)標(biāo)識(shí)圖,并對(duì)該模型的動(dòng)態(tài)特性進(jìn)行了初步分