通信協(xié)議驗(yàn)證中形式化描述方法集成理論的研究.pdf

1、協(xié)議是計(jì)算機(jī)網(wǎng)絡(luò)和通信的核心.研究形式化的協(xié)議理論對(duì)保證網(wǎng)絡(luò)和通信的質(zhì)量、網(wǎng)絡(luò)和信息安全具有十分重要的理論意義和應(yīng)用價(jià)值.該文提出了一種形式化描述方法集成的方法,并為此提供了一致的形式化語(yǔ)義基礎(chǔ).該論文的主要工作包括:1.提供形式化描述語(yǔ)言集成的基本理論依據(jù) 該文通過(guò)收集、整理,總結(jié)出形式化描述語(yǔ)言的一般性定義,并從該定義出發(fā),對(duì)形式化描述語(yǔ)言進(jìn)行了認(rèn)真地剖析和研究,了解各種形式化描述語(yǔ)言之間產(chǎn)生差異的根源,并引入可以將被描述對(duì)象劃分成

2、等價(jià)類的語(yǔ)義抽象函數(shù),將其作為把不同形式化描述語(yǔ)言聯(lián)系起來(lái)的工具,為形式化描述方法的集成提供基本的理論依據(jù).2.提出一種形式化描述方法集成的方法 形式化描述方法的集成主要有兩類方式:集成兩種或多種形式化描述方法形成一種新的形式化描述方法;將一種或多種形式化描述方法與一種或多種半形式化方法集成.該文主要研究第一類方式,并且提出了一個(gè)獨(dú)立各種具體的形式化描述方法的集成方法.3.確立一致的形式化語(yǔ)義域基礎(chǔ) 一致的形式化語(yǔ)義基礎(chǔ)是該文提出的形式

3、化描述方法的集成方法的基石.任何特定對(duì)象的語(yǔ)義都是由計(jì)算這個(gè)對(duì)象的屬性得到.所謂一致的形式化基礎(chǔ),就是通過(guò)對(duì)系統(tǒng)屬性的劃分,對(duì)系統(tǒng)的各種屬性概念進(jìn)行形式化描述和定義,形成聯(lián)系各種形式化描述語(yǔ)言的語(yǔ)義基礎(chǔ),進(jìn)而形成一個(gè)形式化的框架,為各種形式化描述語(yǔ)言的比較、集成提供理論依據(jù).復(fù)雜通信協(xié)議系統(tǒng)的各種屬性總的來(lái)說(shuō)可以被劃分為兩類:系統(tǒng)的行為屬性和系統(tǒng)的結(jié)構(gòu)化屬性.為了將通信協(xié)議系統(tǒng)各種屬性特征抽象出來(lái),我們分別在不同的抽象層次上給出了四種行

4、為形式化模型和兩種結(jié)構(gòu)形式化模型.4.Petri網(wǎng)和Z語(yǔ)言的集成 應(yīng)用該文提出的形式化描述方法的集成方法,我們集成了Petri網(wǎng)和Z語(yǔ)言這兩種目前已經(jīng)相當(dāng)成熟的形式化描述方法,形成一種新的、集成的形式化描述方法PetriZ網(wǎng),并給出了它的形式化定義.PetriZ網(wǎng)一方面可以看作是Petri網(wǎng)在數(shù)據(jù)和函數(shù)定義等系統(tǒng)結(jié)構(gòu)方面的擴(kuò)展;另一方面,PetriZ網(wǎng)也是Z語(yǔ)言在并發(fā)技術(shù)方面的一種擴(kuò)展.使用PetriZ網(wǎng),我們可以對(duì)復(fù)雜的通信協(xié)議系統(tǒng)的