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

1、該文所要研究的是基于RSL的協(xié)議形式化描述技術,這是第一次將RSL引入協(xié)議工程領域.作為RAISE規(guī)范語言的RSL在進行協(xié)議描述時有著兩個獨有的優(yōu)點:廣譜性,這使得在進行協(xié)議描述時可以根據需要進行合理的抽象,從而在各個開發(fā)階段,都可以使用RSL,使整個開發(fā)過程處于同一語義框架之下;描述手段的豐富與靈活,在使用RSL進行協(xié)議描述時,可以根據需要選用合適的語義模型,以最充分的表達協(xié)議內容與協(xié)議性質.此外,RAISE為RSL提供了一些工具,這

2、也為協(xié)議開發(fā)中的自動化工作提供了基礎.該文的研究工作主要集中在以下三個方面:(1)對RSL進行擴充RSL中缺乏時間描述機制,這是在協(xié)議描述中必須解決的第一個問題.該文設計了兩個方案對其進行擴充.一個是引入時間類型Time和系統(tǒng)輔助函數SystemTime.該方案的優(yōu)點在于Time是RSL固有類型Nat的子類型,它的引入不會影響到RSL原有的語法、語義架構和證明系統(tǒng),缺點在于對描述的可讀性和廣譜性有所影響.一個是引入wait表達式.該方案

3、的優(yōu)點在于可讀性強,缺點在于它的引入影響了RSL原有結構,需要對引入后RSL的語法、語義進行討論.RAISE提供的工具也要進行相應的修改.(2)使用擴充后的RSL對協(xié)議進行描述;擴充后的RSL有著較豐富的描述手段和較強的描述能力.能夠適用多種語義模型.該文研究了兩類最基本的模型一基于狀態(tài)機模型和基于進程模型的描述方法.在實際描述中,可以靈活的綜合使用這兩類模型.該文還討論了一種基于輸入/輸出動作序列的描述方法,這是該文中要討論的協(xié)議測試