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

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

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

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

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