網絡實時系統的一種活動性描述語言

摘要:介紹了ADL，它是一種基于網絡實時系統的活動性描述語言，一種描述并發處理中時態和功能行為的新的形式規格說明符號#65377;ADL專用于計算機網絡，是DORIS的一種形式語言擴充#65377;它組合了狀態機活動(ASM)的圖形符號和基于模型的活動功能行為(AFB)符號;提供了關于ASM的抽象語法和靜態#65380;動態語義#65377;最后通過一個小實例說明該語言是如何解釋指定網絡實時系統的#65377;

關鍵詞:結構描述語言; 形式規格說明; 實時處理

中圖分類號:TP393文獻標志碼:A

文章編號:1001-3695(2007)04-0288-04

隨著通信技術和計算技術的發展，基于網絡的實時系統發展迅速，應用廣泛#65377;這些應用依賴于高性能#65380;高可靠性的QoS和端到端高帶寬的數據傳輸，因此開發網絡實時系統的應用程序難度大，對設計#65380;實現和測試的技術及工具要求高#65377;而形式化開發方法是實現軟件自動化的基礎#65377;使用形式化驗證方法可以有效地避免軟件設計錯誤#65377;

由于各種網絡系統復雜性的提高，系統出現故障的可能性也相應增加#65377;其中并發問題通常是不可避免的#65377;如果因并發問題而造成系統故障使某些任務不能在其時限內完成，就有可能造成很大的損失，甚至會危及生命#65377;為了避免出現此類故障，對關于并發實時行為進行形式化的指定和推理是必要的#65377;ADL就是一種描述并發處理中時態和功能行為的新的形式規格說明符號#65377;

1ADL及應用

ADL是一種基于網絡的實時系統規格說明語言#65377;它與DORIS設計方法綜合應用，組合了基于模型的活動功能行為(AFB)符號和狀態機活動(ASM)的圖形符號;給出了關于ASM的抽象語法和靜態#65380;動態語義;能夠正確地描述并行處理中時態和功能行為的新的形式規格說明符號#65377;ADL具有如下特點:①表達力強#65380;簡明直觀#65377;采用端口#65380;變量#65380;操作#65380;狀態#65380;轉變#65380;初始六個元組及相關協議#65380;定理來規格說明系統的活動與屬性#65377;有圖形語法，也有文本語法，簡單明確#65380;易于閱讀#65377;②對模式及并發特征的描述提供支持，給出語言的形式語義#65377;③有完整的無時間限制的證明#65380;語義理論證明#65380;安全證明#65377;④與DORIS設計方法并用，可描述重復活動^[1]#65377;⑤適用于小型網絡系統的規約#65377;

1.1機器狀態活動(ASM)符號

一個ASM規格說明的圖形表示法如圖1中活動A1的圖解#65377;圓表示一個活動;圓周上的實心圓表示端口;橢圓表示靜態;矩形表示動態;矩形上端的左#65380;右手拐角處分別用適當的端口名記錄是否與動態關聯的輸入和輸出，一個端口定義一個與數據流連接的活動界面#65377;雖然用端口能將DORIS與網絡完全鏈接^[2]，但在本文中，端口協議總是一對一的#65377;矩形底部左#65380;右手拐角處分別記錄了動態的時間上#65380;下界限#65377;數據流指被端口名引用的一種活動，用箭頭表示或是在端口用表示DORIS中一個協議符號來標記#65377;這是DORIS設計符號的標準(表1)#65377;初始狀態是一個沒有轉變原因的目標，如圖1中的狀態A#65377;

圖1中活動A1從狀態A開始，它停留在那里直到從P1端口的一個刺激事件發生，然后進入狀態B，狀態B從P1讀出，寫入P2和讀出端口P1，在U1時間單元后退出B狀態;P2與一個通道(無數據通道)協議相連接，即沒有任何空間可以(value B generates產生B值?)#65377;在這種情況下，活動在狀態C等待著從通道釋放事件，以表明現在空間是可用的#65377;

1.2ASM 抽象語法和靜態語義

一個ADL規格說明的六個元組，通過mkADL(端口，變量，操作，狀態，轉變，初始)給出，由源狀態和目標狀態(不用字段.src和.tgt標記)或用它們的標號(不用.label字段標記)來輪流表現轉變特性#65377;以下給出了圖1中活動A1的ASM抽象語法和靜態語義#65377;

(1)類型說明

(2)功能說明

(3)類型

1.3ADL動態語義

1.3.1語義邏輯

ADL用許多種擴充為算術的經典邏輯^[3]表示#65377;實時邏輯:RTL;發生關系:θ^[4，5];相關事件:e;發生次數:i;發生時間:t#65377;θ(e，i，t)表示事件e在時間t發生了ith次#65377;θ是屬性，通過兩個定理給出:

RTLAx 1.任意i:Occ，t1，t2: Time，e: Event#8226;(θ(e，i ，t1)^θ(e，i，t2))t1=t2

RTLAx 2.任意i:Occ，t1:Time，e:Event#8226;(θ(e，i，t1)^ i>1)存在t2:Time#8226;(θ(e，i-1，t2)^t2

擴充實時邏輯:ERTL;保持關系:Φ^[6];P是一個無時限謂語(不包含發生或保持關系)#65377;Φ(P，i，t)表示謂語P在時間t是真實ith的時間#65377;Φ是屬性，通過四個定理給出:

1.3.2語義功能

ASM符號的語義用描述語義功能符Ω來定義#65377;它由一組定理模式組成#65377;Ω是用下面的完全進入↑和離開↓及共同范圍來定義#65377;↑，↓:狀態→事件#65377;

離開動態時，轉變也發生了，當活動在這一時刻仍處于靜態，它就被退出，接著就能瞬時穿過靜態#65377;簡碼在下面定理模式中，在ASM中的這組轉變中將作為ts被提及#65377;

ASM語法屬性的四個功能定義(用來守衛下面的定理模式):

1.3.3狀態機的定理

分為啟動#65380;退出狀態#65380;進入狀態#65380;處理狀態#65380;穩定狀態定理五個部分#65377;靜態語法的警戒在每一模式開始時用方括號表示#65377;SE代表單個入口，SX代表單個退出#65377;

(1)啟動定理

定理1[true] θ(↑ initial， 1， 0) 

(2)退出狀態定理

定理2[isStaticState(s.s)，TransitionsOut(s，ts)≠，st∈Successors(s，states，ts)]

任意i: Occ，t : Time#8226;θ(↓s，i ，t )

定理3[isDynamicState(s.s)]

任意i : Occ，t : Time#8226;

(3)進入狀態定理

定理4[s=initial]

任意i: Occ，t : Time#8226;(i>1∧θ(↑s，i，t)存在ss∈Predecessors(s， states， ts)) #8226;

定理5[s≠initial]

任意i: Occ，t: Time#8226;θ(↑s，i，t)存在ss∈Predecessors(s，states， ts)#8226;

(4)處理狀態定理

定理6[isDynamicState(s.s)]

任意i : Occ，t : Time#8226;θ(↑s，i，t)存在t1: Time#8226;t+s.timing.dmin≤t1 ≤t + s.timing.dmax∧θ(↓s，i，t1)

定理7[isStaticState(s.s)，tr∈TransitionsOut(s，ts)， isEvent(tr.label.l)，tr.label.l=e]

任意i: Occ，t : Time #8226;θ(e ，i，t)θ(↓s，i，t)

定理8[isStaticState(s.s)，isTimeBounds(tr.label.l)，tr.label.l=(l，u)]

任意i:Occ，t:Time#8226;θ(↑s，i，t)存在t1: Time#8226;t+l≤t1≤

t+u∧θ(↓s，i，t1)

(5)穩定狀態定理

定理9[isDynamicState(s.s)]

任意i: Occ，t : Time#8226;θ(↓s，i，t)存在t1: Time#8226;ts.timing.dmax≤t1≤ts.timing.dmin∧θ(↑s，i，t1)

定理10[isStaticState(s.s)，card Successor(s，states，ts)≠

任意i: Occ，t : Time#8226;θ(↓s ，i，t)存在t1: Time#8226;t-u≤t1 ≤t-l∧θ(↑s，i，t1)

定理11[isStaticState(s.s)，card Successor(s，states，ts)≠φ，isEvent(tr.label.l)，tr.label.l=e]

任意i: Occ，t : Time#8226;θ(↓s，i，t)存在j:Occ#8226;ins (s，i，t )∧θ(e，j，t)

定理12[isStaticState(s.s)，card Successor(s，states，ts)=φ]

任意i: Occ，t : Time#8226;┐θ(↓s，i，t)

1.4活動功能行為(AFB)符號

AFB符號是用一個時間的前后關系去解釋，標準的VDMSL是無時間的#65377;AFB基于VDMSL的一組子集和對完整的VDMSL的一個簡單理論證明#65377;它描述一組有效的活動是由一個VDMSL模塊組成，其類型和狀態被用于描繪活動的邏輯狀態#65377;模塊的操作與ASM的動態相關#65377;如果相應的動態只有一個輸入#65380;一個輸出，那么該操作將只有一個輸入參數和一個輸出結果#65377;AFB操作是在時間框架內用ASM符號定義來解釋的#65377;特殊地，當狀態離開(不假設前條件保持進入)時，將保持后條件#65377;

1.5DORIS通道協議及通道定理

1.5.1DORIS通道協議

DORIS活動不能被直接連接在一起，它們必須以一個特殊協議(通道)來通信(DORIS 協議在RTL中有一個理論語義證明^[7]，并廣泛接受BSI標準的考驗)#65377;DORIS通道協議用三種寫入和三種讀出事件表述其特性#65377;寫出事件:寫入數據開始，wds;寫入數據結束，wde;寫入結束，we#65377;讀出事件:讀出開始，rs;讀入數據開始，rds;讀入數據結束，rde#65377;每種協議也由兩個事件表現其特性:項目寫入，iw;項目讀出，ir#65377;由記錄一個項目被寫入或從一個協議讀出的事件#65377;

一個DORIS通道獨特的地方在于它支持兩個特殊的儲藏單元:一個是當通道滿時，可以被放置在一個數據項目中;一個是當被讀出時，被放置在一個數據中#65377;雖然生產者可以寫入特殊單元，但直到消費者開始讀出一些數據時，它才被釋放出來#65377;wde與we的區別是當通道沒有滿時，它們是一致的#65377;rs與rds事件是不同的:當試圖制造開始讀入時，rs發生(雖然在通道中，也許沒有任何數據)，并且當數據開始被讀入時，rds發生#65377;數據存在開始讀出時，rs與rds是一致的#65377;讀出儲藏單元，承認讀出事件的開始，rs釋放一個保持的寫入#65377;

1.5.2通道定理

通道定理認為是瞬時通信#65377;例如，一旦一個rs事件出現，就被寫入檢測#65377;

1.6ADL在網絡實時系統中的應用

下面，舉一個小的實例(圖1)說明ADL是如何解釋指定的實時系統#65377;例子的理論生成#65380;典型無時間限制和安全保護已被形式化和證明#65377;圖1的網絡是由通過一個通道鏈接的兩個簡單活動組成#65377;從一些輸入傳感器到達一個新目標圖像觸發活動A1，完成一些圖像處理以決定目標的位置#65377;這些位置穿過通道到達A2，A2計算目標如何移動，并且把這個向量輸出到系統其他地方#65377;形式化說明如下:

活動A1的描述定理

其中，通道可通過下面的鏈接定理形式化:

2結束語

簡單動態只有一種關聯操作，最多只能參考一個輸入端口和一個輸出端口#65377;進入狀態時，通過簡單的VDMSL^[8，9]操作使其對動態功能的描述成為可能#65377;一個完整的動態有兩個或更多的關聯操作，這些可在任何一個命令中被執行#65377;由于篇幅所限，在這里僅借助一個簡單實例，介紹ADL是如何描述一個網絡系統的#65377;在未來的研究中，對稍微大一點#65380;復雜一點的系統如何很好地增加ADL規模的研究是必需的，特別是在系統功能和時序相互作用上更加重要#65377;

本文中所涉及到的圖表、注解、公式等內容請以PDF格式閱讀原文。