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

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

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

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

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