基于組件自動機的概率連續行為的形式化模型

卜星晨，曹子寧，王福俊

(南京航空航天大學 計算機科學與技術學院，江蘇 南京 211106)

0 引 言

基于組件的開發技術正逐漸應用到信息物理融合系統(CPS)[1-2]的開發過程中。現已有許多基于組件的軟件系統開始應用到航空航天、軍事過程控制等領域當中，這些領域往往對系統的正確性和可靠性要求比較高。系統執行過程中的一個小小的錯誤都有可能導致巨大的災難。而這類系統往往同時具有連續性和離散性，且每個子系統之間存在著頻繁的數據通信，因而給這類系統的準確建模帶來了一定的困難。

基于組件[3-4]的開發技術是一種將系統組件化、然后再將組件化后的系統組件進行組合的技術。采用形式化的方法[5]對CPS進行建模與驗證，能夠很好地保證系統的正確性和安全性。形式化的驗證過程一般采用形式化建模語言對系統進行建模，采用邏輯語言刻畫所要驗證的性質，最后使用形式化驗證工具自動地對模型和邏輯規約進行驗證。文獻[6]指出在基于組件的開發過程中引入形式化的建模方法和自動化驗證技術，是一個重要的研究方向。

該文針對CPS，在組件自動機的基礎上擴展了概率、連續行為特性，提出了概率混成組件交互自動機，并給出了具體的定義及其進行組合驗證的算法。提出的概率混成組件交互自動機不僅能夠描述組件之間的交互行為，還能能夠清楚地刻畫出系統的體系機構以及組件內的連續動態性和狀態遷移上的概率選擇性。

1 背景和動機

CPS是一種將計算過程與物理過程組合在一起的實時反應式系統。其最主要的特征是系統中同時包含離散性和連續性。CPS本身是一種基于組件的系統，每一個軟件實體或者物理設備都能夠獨立運行，每個子系統之間可以通過信號的傳輸實現相互合作的功能。

現已有許多能夠對混成系統進行建模的形式化方法，如混成自動機[7-8]和混成I/O自動機[9-10]。然而混成I/O自動機是輸入使能的，即混成I/O自動機中的每一個狀態都必須能夠接收所有可能的輸入動作，而混成自動機并不能夠將組件之間的通信組合方式進行準確建模。因此，需要一種新的形式化建模方法對CPS進行建模。

組件交互行為的建模方法可以分為兩大類：基于進程代數的方法和基于自動機的方法。基于進程代數的方法主要使用CSP/Timed CSP、Pi演算、CCS/Timed CCS等進程代數語言進行建模。基于自動機的方法主要使用接口自動機[11]、I/O自動機、時間自動機[12]以及時間I/O自動機[13]進行建模。組件交互自動機[14-16]在自動機的基礎上根據進程代數的思想擴充了組件之間交互行為的描述，使其能夠保留組件之間的交互屬性。

1.1 組件交互自動機

組件交互自動機是一種非確定的自動機，其中每一個遷移動作都標注為輸入、輸出或者內部動作。輸入(輸出)動作與接收(發出)該動作的組件相關聯。內部動作與動作上同步的兩個組件相關聯。在組件交互自動機的一次組合過程中，只有兩個組件可以進行同步操作。組件交互自動機的定義如下：

定義1：組件交互自動機COIA可以寫成元組的形式(Q,Q0,A,Σ,E,H)，其中：

(1)Q表示非空的有限狀態集合；

(2)Q0?Q表示初始狀態集合；

(3)A表示有限動作集，包括輸入動作、輸出動作、內部動作τ和空動作ε；

(4)Σ表示動作約束符號表的集合，Σ={(C)×A×(C∪(±))}，C表示組件及其接口的名稱，C∈N(H)，N(H)表示組件組合過程中涉及到的組件名稱的集合，+和-分別表示輸入動作和輸出動作；

(5)E?Q×Σ×Q，表示狀態遷移的集合；

(6)H是用來表示組件內部組件組合層次的元組，元組Hi=(ni1,ni2,…,nim)表示組件Hi由m個組件在同一層次上組成而成。括號用來表示組合的層次性，最內層的組件最先進行組合，然后依次向外進行組合。

(A,a,+),(B,a,-),(B,a,A)∈E分別表示輸入、輸出和內部動作。(A,a,+)表示組件A接收動作a，(B,a,-)表示組件B發送動作請求a，(B,a,A)表示組件B輸出動作a，組件A接收到動作a。

1.2 動 機

CPS是基于組件的系統，這為使用COIA對CPS進行建模提供了良好的基礎。現有的組件交互自動機只支持離散系統的建模，并不支持概率以及連續行為性質的建模。因此，對組件交互自動機進行了相應的擴展，在組件交互自動機的基礎上提出了概率混成組件交互自動機PHCOIA來對CPS進行建模。

2 概率混成組件交互自動機

PHCOIA在COIA的基礎上添加了變量集X，變量集X的不同取值表示系統所處的不同狀態。PHCOIA在COIA的基礎上對狀態上的動作變遷，增加了關于變量集合X的約束條件Enab，只有滿足了相應的約束條件之后，才能執行動作進行狀態變遷。

現實生活中總會存在一些不確定因素對系統的執行造成一定的影響，因此在COIA的狀態遷移上添加了概率分布P，表示狀態變遷上的不確定選擇。除此之外，還定義了賦值函數Fa和流函數F分別表示對狀態內變量的賦值操作以及定義狀態內變量的變化速率。通過定義不變式I約束每個狀態內變量的變化范圍。PHCOIA的定義如下：

定義2：PHCOIA可以寫成元組的形式(Q,Q0,A,Σ,X,Xinit,Fa,F,Enab,E,I,P,H)，其中：

(1)Q表示非空的有限狀態集合；

(2)Q0?Q表示初始狀態；

(3)A表示有限動作集，包括輸入動作Ain、輸出動作Aout、內部動作Aint和空動作ε；

(4)Σ表示動作約束符號表的集合， Σ={(C)×A×(C∪(±))}，C∈N(H)；

(5)X表示實值變量的有限集合；

(6)Xinit表示變量集合X在初始狀態的取值；

(7)Fa:Q→assign(X)表示賦值函數，用來對狀態中的變量進行賦值；

(8)F:Q×|X|→|X|表示狀態上變量的流函數，F函數定義了變量的變化率，通常使用變量對時間的一階導數進行表示；

(9)Enab:Q×Σ→guard表示狀態執行動作遷移的謂詞條件，guard為變量集合X上的布爾表達式；

(10)E表示狀態遷移的集合，E?Q×Σ×Q'；

(11)I為狀態q?Q上的不變式條件，用來限制變量的變化范圍，不變式條件通常使用變量集合X上的布爾表達式進行表示；

(13)Η是描述該組件內組件組合層次的元組。

3 PHCOIA的遷移系統語義

PHCOIA中的狀態由系統當前所處位置q∈Q和變量的取值組合而成。PHCOIA中有兩種遷移方式：動作遷移和時間遷移。動作遷移：當狀態內的變量值滿足相應的謂詞條件guard時，當前狀態將會執行動作Σ跳轉到下一個狀態；時間遷移：系統停留在當前位置q，但系統中的變量隨著時間的流逝不斷地發生變化。時間遷移的邊標記為實數值，表示系統在位置q上停留的時間。Δ表示所有遷移邊的集合，Δ=Σ∪R≥0。

PHCOIA的遷移系統從初始狀態S0開始執行，如果當前狀態滿足動作遷移的使能條件Enab，系統將會根據概率分布P從所有可能的后繼狀態中選擇一個狀態進行跳轉；如果當前狀態不滿足變遷的使能條件，狀態將會執行時間遷移，狀態內的變量根據流函數隨著時間的變化而發生變化。

時間延遲只發生在位置上，動作變遷的時間忽略不計。因此，如果不對狀態變遷進行進一步的約束，就有可能出現自動機在有限時間內執行無限多動作的情況，即Zeno行為。然而現實生活中這樣的情況是不存在的，即不存在可以在有限時間內執行無限多指令的計算機。因此，接下來給出結構良好性標準。

定義4：如果對于TR(M)中的所有狀態s，滿足?n∈，?π∈π(s)，?i∈，durπ(i)>n，即對于任意給定的時間n∈，總是存在一條從狀態s開始的路徑π(s)，從狀態s到達路徑π(s)上某一狀態的時間大于n，則稱PHCOIA滿足結構良好性標準。

該文所定義的PHCOIA不包含齊諾行為。只有滿足結構良好性標準的PHCOIA才能進行有效的組件組合。

4 PHCOIA的組合與驗證

4.1 PHCOIA組合的相關概念

在交互自動機的組合過程中，需要匹配對應的輸入輸出動作。在狀態的組合過程中，除了需要組合狀態內的變量集外，還需要組合狀態上的賦值函數、流函數和不變式約束，同時在生成的狀態集上生成對應的遷移關系以及對應的概率分布，以構造新的組件自動機。

定義5：如果兩個狀態內的賦值函數、流函數和不變式約束中出現的變量集合不相交，則稱這兩個狀態可以進行組合。

定義6：PHCOIAM有輸出動作(Ci,αi,-)∈ΣM，i∈，PHCOIAN有輸入(Ck,αk,+)∈ΣN，k∈。將M和N進行組合，如果αi和αk動作名稱相同且輸出動作αi前后兩個狀態可以與輸入動作αk前后兩個狀態分別進行組合，則稱輸出動作αi與輸入動作αk匹配。在不考慮內部動作細節的情況下，內部動作可以簡記為(Ci,τ,Ck)。

定義7：D(H)表示組件組合層次的深度。H=(C)，表示H內只有一個元素C，即該組件是一個原子組件，組件的組合深度為1。

定義8 ：PHCOIA的組合S=(Q,Q0,A,Σ,X,Xinit,Fa,F,Enab,E,I,P,H)，是由PHCOIA的集合{Mi=(Qi,Q0i,Ai,Σi,Xi,Xiniti,Fai,Fi,Enabi,Ei,Ii,Pi,Hi)}組合而成，其中：

(1)i∈N且參與組合的組件名稱集合{(N(Hi))}互不相交；

(3)動作約束符號Σ?{C×A×(C∪(±))}，C∈N(Hi)∪N(Hk)；

(5)Fa,F,I分別為組合后狀態上的賦值函數、流函數以及不變式約束；

(6)H為組件內組件組合層次的元組。

在自動機的組合過程中，需要考慮動作的匹配，如果兩個自動機存在可以匹配的動作，且這兩個動作的使能條件可以同時滿足時，這兩個動作可以同步生成為一個內部動作；如果兩個動作不匹配，那么這兩個動作將會交替執行下去。兩個自動機在組合過程中既可能存在同步互補動作，也可能存在交替執行動作。

4.2 PHCOIA的組合算法

PHCOIA組合算法，將M1,M2進行組合，M1=(Q1,Q01,A1,Σ1,X1,Xinit1,Fa1,F1,Enab1,E1,I1,P1,H1),M2=(Q2,Q02,A2,Σ2,X2,Xinit2,Fa2,F2,Enab2,E2,I2,P2,H2),輸出為組合后的自動機S=(Q,Q0,A,Σ,X,Xinit,Fa,F,Enab,E,I,P,H)。下面給出PHCOIA組合算法的具體步驟：

2、從自動機M1和M2的初始狀態進行狀態組合，如果M1和M2的初始狀態不能進行組合，則返回錯誤信息；否則標記Q01和Q02，自動機S的初始狀態Q0為Q01和Q02的狀態組合，將Q0添加到狀態集合Q中，狀態Q0內部的初始變量賦值Xinit等于Q01和Q02狀態內變量的初始值，狀態Q0內的賦值函數、流函數以及不變式約束分別為Q01和Q02上賦值函數的并集、流函數的并集和不變式約束的并集；將狀態S1,S2,SPre分別置為Q01,Q02和Q0，跳轉到步驟3；

3、如果M1和M2中的狀態都被標記過，則H=(H1,H2)，組合完成程序返回；如果S1,S2都存在后繼狀態變遷，則跳轉到步驟4；如果S1存在狀態變遷而S2不存在，則跳轉到步驟8；如果S1不存在狀態變遷而S2存在，則跳轉到步驟9；如果都不存在變遷，程序返回；

7、步驟7的內容與步驟6的內容相似，不再重復贅述；

9、步驟9的內容與步驟8的內容相似，不再重復贅述。

4.3 PHCOIA的組合驗證

PHCOIA的組合算法通過遍歷自動機中的所有遷移來實現兩個自動機的兼容性組合。利用該算法可以直接對兩個PHCOIA進行組合相容性錯誤檢測。如果在組合過程中，需要組合的兩個狀態內包含的變量有交集，或者在動作的組合過程中，當前自動機中的同步動作與目標自動機在保證動作先后序列的前提下無法找到與之匹配的動作或者兩個同步動作不匹配，則判定出現相容性錯誤，給出錯誤提醒。

5 基于PHCOIA的應用實例

本節使用PHCOIA對飛行器的對接過程進行建模。在兩個飛行器的對接過程中，后面追趕的飛行器稱作追趕者飛行器(chaser),需要對接到的飛行器稱為目標飛行器(target)，追趕者沿著半徑為r1的軌道以角速度θ1運行。為了順利地與目標飛行器完成對接，追趕者需要先在低軌道上改變自身的角度姿勢，然后再逐漸上升到目標飛行器所在的高度進行對接。當上升到一定高度之后，追趕者將發送對接信號dock與目標飛行器進行對接。飛行器的每一次對接并不能保證完全的成功，存在一定的失敗機率。如果對接失敗，目標飛行器將會發送失敗信號error，追趕者接收到信號后將會下降自身高度，重新調整角度，準備下一次的對接；如果對接成功，追趕者將會收到目標飛行器發送的對接成功信號success，并與目標飛行器以相同的角速度一同運行下去。

追趕者的PHCOIA如圖1所示，目標飛行器的PHCOIA如圖2所示。

圖1 追趕者飛行器的PHCOIA

圖2 目標飛行器的PHCOIA

兩個飛行器的組合建模如圖3所示。為了建模的簡單呈現，所有的輸入輸出動作都組合成了內部動作。從組合后的PHCOIA中，可以很直觀地看出對接過程中，各個系統內部的連續變化特性以及狀態遷移上的概率不確定性，同時系統內部各個組件的交互行為也能夠通過組件交互自動機很好地保存下來。

圖3 組合后的PHCOIA

6 結束語

在COIA的基礎上，針對CPS，提出了概率混成組件交互自動機的概念。PHCOIA不僅能夠詳細地描述組件之間的交互行為，還能夠清楚地刻畫出組件狀態內的連續變化特性以及狀態變遷上的概率選擇性。可以利用PHCOIA對CPS中的各個組件進行準確建模。在給出PHCOIA的相關定義之后，還給出了其相應的組合算法，根據組合算法可以將表示各個組件的自動機進行組合，從而構建出一個完整的表示原系統的PHCOIA。在接下來的工作中，將著手在PHCOIA上開展形式化驗證的研究，使其能夠在PHCOIA上驗證相關性質。