基于RSL的協(xié)議形式化描述方法研究.pdf

1、協(xié)議工程是一體化、形式化的協(xié)議開(kāi)發(fā)過(guò)程。協(xié)議的開(kāi)發(fā)主要包括了協(xié)議設(shè)計(jì)、協(xié)議描述、協(xié)議驗(yàn)證、協(xié)議實(shí)現(xiàn)、協(xié)議測(cè)試和協(xié)議維護(hù)等過(guò)程。這里“一體化”的含義就是：協(xié)議開(kāi)發(fā)的各個(gè)過(guò)程在技術(shù)上前后銜接，并在同一個(gè)開(kāi)發(fā)系統(tǒng)中完成?！靶问交眲t指的是：用形式化描述語(yǔ)言FDL連接協(xié)議開(kāi)發(fā)的各個(gè)階段。
　　 在協(xié)議工程中，形式化描述技術(shù)占據(jù)了核心地位，它貫穿于整個(gè)開(kāi)發(fā)過(guò)程的始終，因而它也是這一領(lǐng)域的研究熱點(diǎn)。目前已有的一些協(xié)議形式化描述模型主要有：基

2、于狀態(tài)機(jī)的各類FSM、各類PetriNet，基于進(jìn)程代數(shù)的CCS、CSP，時(shí)序邏輯TL等等。協(xié)議形式化描述語(yǔ)言則主要有Lotos、Estelle、SDL等。由于各種方法在協(xié)議描述與分析時(shí)有著各自的優(yōu)、缺點(diǎn)，目前還沒(méi)有一種方法能夠完全滿足協(xié)議工程的需要。
　　 本文所要研究的是基于RSL的協(xié)議形式化描述技術(shù)，將RSL引入?yún)f(xié)議工程領(lǐng)域。作為RAISE規(guī)范語(yǔ)言的RSL在進(jìn)行協(xié)議描述時(shí)有著兩個(gè)獨(dú)有的優(yōu)點(diǎn)：廣譜性，這使得在進(jìn)行協(xié)議描述時(shí)可

3、以根據(jù)需要進(jìn)行合理的抽象，從而在各個(gè)開(kāi)發(fā)階段，都可以使用RSL，使整個(gè)開(kāi)發(fā)過(guò)程處于同一語(yǔ)義框架之下；描述手段的豐富與靈活，在使用RSL進(jìn)行協(xié)議描述時(shí)，可以根據(jù)需要選用合適的語(yǔ)義模型，以最充分的表達(dá)協(xié)議內(nèi)容與協(xié)議性質(zhì)。
　　 本文的研究工作主要集中在以下三個(gè)方面：首先對(duì)RSL進(jìn)行添加。RSL中缺乏時(shí)間描述機(jī)制，這是在協(xié)議描述中必須解決的一個(gè)問(wèn)題。本文設(shè)計(jì)了兩個(gè)方案對(duì)其進(jìn)行添加。一個(gè)是引入時(shí)間類型Time和系統(tǒng)輔助函數(shù)System

4、Time。該方案的優(yōu)點(diǎn)在于Time是RSL固有類型Nat的子類型，它的引入不會(huì)影響到RSL原有的語(yǔ)法、語(yǔ)義架構(gòu)和證明系統(tǒng)，缺點(diǎn)在于對(duì)描述的可讀性和廣譜性有所影響。一個(gè)是引入wait表達(dá)式。該方案的優(yōu)點(diǎn)在于可讀性強(qiáng)，缺點(diǎn)在于它的引入影響了RSL原有結(jié)構(gòu)，需要對(duì)引入后RSL的語(yǔ)法、語(yǔ)義進(jìn)行討論。RAISE提供的工具也要進(jìn)行相應(yīng)的修改。然后用改進(jìn)后的RSL對(duì)協(xié)議進(jìn)行描述。改進(jìn)后的RSL有著較豐富的描述手段和較強(qiáng)的描述能力。能夠適用多種語(yǔ)義模型