面向CPS的混成AADL建模與模型轉換

曹雪岳，曹子寧，卜星晨

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

0 引 言

信息物理融合系統(tǒng)(cyber-physical system，CPS)[1]是信息系統(tǒng)和物理設施高度融合和深度協(xié)作的新型工業(yè)系統(tǒng)。CPS采用計算、通信和控制結合的3C結構[2]，系統(tǒng)不僅包含離散的計算過程，還包含連續(xù)的物理事件。CPS已經廣泛應用于航空、醫(yī)療、交通等領域。目前國內對CPS的研究方向集中在系統(tǒng)的建模與仿真、網(wǎng)絡構建安全性驗證上[3]，其中系統(tǒng)的建模是其他研究的基礎。目前對CPS的形式化建模方法有混成自動機[4]、微分動態(tài)邏輯[5]、HCSP[6]等。

體系化結構分析與建模語言(architecture analysis & design language，AADL)[7]是美國汽車工程協(xié)會SAE在2004年建立的一套適用于嵌入式實時系統(tǒng)的建模規(guī)范。AADL建模語言具備對系統(tǒng)硬件和軟件建模的能力，同時能夠支持組件建模，可以將組件系統(tǒng)作為軟件組件在執(zhí)行平臺的映射。由于AADL缺乏形式化語義無法直接對其進行模型檢測或者定理證明，文獻[8]將AADL行為附件轉換為實時進程代數(shù)stateful timed CSP，通過模型轉換對非線性F-16模擬系統(tǒng)進行安全性驗證。文獻[9]中結合Z語言提出了AADL非功能屬性的形式化描述Z-AADL，并提出其到ZIA的轉換規(guī)則。文獻[10]將AADL建模的嵌入式系統(tǒng)模型轉換為廣義隨機Petri網(wǎng)，使用廣義隨機Petri網(wǎng)對模型進行性能評價。

進程代數(shù)[11]是作為通信系統(tǒng)描述語言被提出的，可以很好地描述系統(tǒng)中的通信、同步和并發(fā)，并且可以使用形式化方法進行推理和驗證。進程代數(shù)也是學術界研究的熱點，各種對經典的進程代數(shù)的擴展被提出，如Timed-CCS、隨機進程代數(shù)、π演算等。同時進程代數(shù)可以對CPS系統(tǒng)中大量存在的并發(fā)與交互給出形式化描述，文獻[12]中結合進程代數(shù)CCS提出一種并發(fā)AADL用于對CPS系統(tǒng)并發(fā)特性的形式化建模。

通過分析CPS系統(tǒng)的特性，文中在CCS的基礎上擴展微分方程和概率選擇，提出CPS系統(tǒng)形式化描述語言HPCCS。擴展AADL行為附件用于描述隨機動作并提出混成附件使其能夠描述物理環(huán)境中的連續(xù)變化和組件間通信。由于AADL是半形式化的，因此有必要將其轉換為形式化語言HPCCS，根據(jù)兩者的語法和語義，提出AADL到HPCCS的轉換規(guī)則，為CPS的形式化驗證和分析奠定基礎。

1 混成隨機進程代數(shù)-HPCCS

進程代數(shù)最早用來刻畫通信系統(tǒng)的行為，可以描述系統(tǒng)的并發(fā)特性。文中在CCS的基礎上提出一種用于CPS系統(tǒng)建模的進程代數(shù)HPCCS。HPCCS能夠描述CPS系統(tǒng)的連續(xù)變化，還可以描述CPS系統(tǒng)中存在的概率行為。本節(jié)將詳細給出HPCCS的語法和操作語義，并給出一個水箱的建模案例。

1.1 HPCCS語法

首先給定一個系統(tǒng)S，存在一個動作集合A={a1,a2,…,an}，系統(tǒng)變量集合分為連續(xù)變量集合Actc={c1,c2,…,cn}和離散變量集合Actd={d1,d2,…,dn}。

定義1：HPCCS語法。

P:=ε//空進程

|a.P//離散動作

|io?(x).P//輸入動作

|io!(x).P//輸出動作

|d>>P//賦值操作,其中d:=[v|Pr]|[Pr]

|c?d>>P//流動作，?P表示P進程可以中斷流動作

|!(P) //遞歸操作符

|P[A] //隱藏算子

|P⊕P//交錯并發(fā)

下面介紹HPCCS引入的新的算子的作用。首先賦值操作算子d>>P，除了能定義變量值的離散變化也可作為條件約束，表示當d中的謂詞公式Pr滿足時繼續(xù)執(zhí)行P進程。具體形式如下：

d::=[v|Pr]|[Pr]

在定義的進程算子的基礎上，通過遞歸定義引入幾個常用算子。首先同步并發(fā)P1|[A]|P2::=P1⊕P2[A]，表示限制P1和P2只能在A動作集同步。然后為HPCCS引入順序操作P1⊙P2，表示P1執(zhí)行完繼續(xù)執(zhí)行P2?？紤]P.a這種形式在HPCCS中是不能出現(xiàn)的，下面采用遞歸的形式給出P.a的定義：

(1)P:=ε,那么P.a:=a；

(2)P:=b.P',那么P.a:=b.(P'.a)；

(3)P:=io?/!(x).P',那么P.a:=io?/i(x).(P'.a)；

(4)P:=d>>P',那么P.a:=d>>(P'.a)；

在得到P.a后可以定義進程間順序組合：

P1⊙P2::=P1.a!⊕a?.P2[a]。

接下來通過水箱系統(tǒng)的例子說明HPCCS的建模能力。水箱系統(tǒng)[13]是由水箱和控制器組成，控制器通過傳感器獲取水位，根據(jù)設定的水位閾值決定是否關閉進水系統(tǒng)。當進水系統(tǒng)關閉時水位由于漏水開始下降。文中在控制器部分引入錯誤，當水位低于最低值的時候由于控制器故障可能不會打開注水閥門，該故障隨機出現(xiàn)，并且出現(xiàn)后可以自動修復，故障率為20%。模型如下：

WTS:=Watertank|[wl,cv]|Controller

Water:=[(v,d)|v+=v0;d+=d0]>>([v=1]>>[d|d'=Qin-πr2×d] ?(wl!(d).cv?(v)))⊙([v-=0]>>[d|d'=-πr2*d]?(wl!(d).cv?(v)))

Controller:=[(v,d)|v+=v0;d+=d0]>>！([t|t+=0]>>[t|t'=1;t<10]⊙(wl?(d)⊙[d->Error)⊙[d->high]>>v=1.cv!(v)))

Error:=v=0.cv!(v) +0.8v=1.cv!(v)

1.2 HPCCS的操作語義

HPCCS的語義是通過結構化操作語義[14]規(guī)則描述。目前形式化描述語義主要有：操作語義、指稱語義、公理語義和代數(shù)語義。操作語義是通過抽象的方法描述語言中每個基本算子的執(zhí)行效果，避免描述的語言依賴于實現(xiàn)的具體計算機系統(tǒng)，一般使用狀態(tài)遷移系統(tǒng)描述。該方法的優(yōu)點在于具有直觀的表現(xiàn)形式。

定義2：標號遷移系統(tǒng)。

標號遷移系統(tǒng)可以表示為四元組：M=，其中Q表示狀態(tài)集合，L表示動作集合，→?S×L×S表示狀態(tài)上的變遷，Q0?Q表示初始狀態(tài)集合。

給定一個HPCCS進程S，可以得到S對應的標號遷移系統(tǒng)T(P)=，構造標號遷移系統(tǒng)的過程如下：

(1)狀態(tài)集Q=subp(P)∪{ε}×V(S)，其中subp(P)表示進程P的所有子進程組成的集合，例如P:=[t|t+=0]>>(?[t>3]>>P)，subp(P')={S,[t>3]>>P,,ε}∪subp(P'),ε表示終止進程。V(S):={v|v∈Var(S)->Val},表示每個狀態(tài)上變量的取值，其中Val表示變量的值域。

(2)L表示HPCCS中的動作，L:=R+∪Channel.{?,!}.R∪Act，由三種動作組成：時間流逝、通信動作、離散的非通信動作。

(3)→表示狀態(tài)上的變遷，→:=S×L×S。

(4)Q0表示初始狀態(tài)，Q0:={(P,s)|s∈V(S)}，其中P表示開始時的進程，s表示此時變量的取值。

定義3：HPCCS的操作語義。

下面給出賦值操作d>>P、流動作c?d>>P、交錯并發(fā)算子P⊕P的操作語義。

2 CPS系統(tǒng)建模工具-混成AADL

2.1 AADL組件的抽象描述

行為附件規(guī)范可以定義為一個三元組：

BA::=(state_variable,State,Trans)

其中state_varibale表示系統(tǒng)中定義的變量集合，State表示系統(tǒng)狀態(tài)集合，Trans表示狀態(tài)中變遷的集合。變遷可以描述為：

Tran::=state1[guard]->state2{action}

行為附件規(guī)范不能描述狀態(tài)上的不確定選擇。文中在行為附件的基礎上引入概率選擇的狀態(tài)集合transient_State，引入新的遷移集合transient_transition。transient_transition?transient_state×R+×State，表示選擇狀態(tài)可以執(zhí)行一個瞬間選擇到一個普通狀態(tài)，例如t1:tS-[5]->S1,t2: tS-[5]->S2。提出擴展隨機選擇的行為附件規(guī)范，定義如下：

定義4：帶隨機選擇的行為附件。

帶隨機選擇行為的行為附件，隨機選擇狀態(tài)集合為Transient _state，附件規(guī)范：

PBA::=(state_variable,State,Transient_state,Trans,Transient_trans)，其中Trans::= state1-[guard]->state2{action}，state1∈State，state2∈State∪Transient_state。

為了使AADL能對CPS系統(tǒng)中的物理行為建模，提出基于HPCCS的AADL混成附件，利用HPCCS流算子對CPS中物理行為建模，利用HPCCS的通信操作可以描述計算組件和物理設備間的數(shù)據(jù)通信。混成附件作為AADL設備組件的注解，對傳感器和執(zhí)行器的連續(xù)行為建?；蛘咦鳛槌橄蠼M件實現(xiàn)。混成附件規(guī)范由三個部分組成：變量，組件的通信接口集合，HPCCS進程描述的行為集合。

定義5：混成附件。

混成附件可以抽象描述為三元組：

HA::=(Variables，Channels，Proc)

其中Variables表示系統(tǒng)中的變量，Proc表示由HPCCS表示的進程組成的集合，用于對物理設備建模。Proc的BNF定義如下:

Proc::=process{&process}

process::=identifier'='expression

expression::=ε'.'expression|io'?('x').'expression|

d'>>'expression|'!('expression')'|

c'@'d'>>'expression|expression';'expression|

r'.'expression{+r'.'expression}

d::='[('x{','x}')|'equation';'guard]'

c::='<('x{','x}')|'flow';'guard>'

Proc中io只能是混成附件中規(guī)定的通道名，也就是Channels中的通道名，Channels是附件中定義的數(shù)據(jù)端口。Channels和Variables的定義和行為附件中保持一致。第三節(jié)給出混成附件對飛行控制系統(tǒng)建模的例子。

2.2 混成AADL到HPCCS的轉換規(guī)則

由于行為附件只會描述系統(tǒng)中的離散行為，所以轉換后的HPCCS不包含連續(xù)變量和流算子。行為附件可以表示為BA=(state_variable,State，Transient_state,Trans,Transient_trans)，其中state_variable表示行為附件中的變量，可以對應到HPCCS中的離散變量。Trans表示變遷，描述了狀態(tài)間的遷移關系，可以描述為進程中的動作。轉換過程如下：

(1)將行為附件中的變量映射到HPCCS中的離散變量集合中。

(2)狀態(tài)集合中的狀態(tài)分別對應一個進程變量。

(3)行為附件中的遷移可以表示為s1-[guard]->s2{act}。其中guard有兩種形式: on dispatch和執(zhí)行條件，前者表示遷移的周期執(zhí)行，后者表示當滿足給定條件是遷移執(zhí)行。所以需要先轉換guard再轉換act。

(3.1)轉換guard：在行為附件中guard代表變遷被觸發(fā)的條件，一般有三種：定時觸發(fā)，條件觸發(fā)，端口上發(fā)生的輸入輸出事件。對于條件觸發(fā)可以對應HPCCS中d的謂詞形式。端口上的輸入輸出對應HPCCS中的輸入輸出事件。對于定時觸發(fā)需要轉換為!([t|t+=0]>>[t|t'=1]?[t>P)。

(3.2)轉換act，行為附件act中的動作可以轉換為HPCCS中d變量的變化。

(4)轉換行為附件中的Transient_trans。

3 基于混成系統(tǒng)的飛行控制系統(tǒng)建模

目前國內外先進飛機配置多達數(shù)千個嵌入式處理器，用于進行實時計算任務。這些嵌入式設備通過處理外界物理信息得到各種飛行任務。現(xiàn)代飛行管理系統(tǒng)(flight management system)如圖1所示[15]。

考慮飛機上升時的操作。首先飛機以平飛的模式到達指定水平位置，控制器驅動飛機進入上升狀態(tài)，開始向上爬升。當達到指定高度后，控制器驅動飛機進入水平飛行狀態(tài)。因此上升操作模式可以抽象出三個狀態(tài)，s1,s2分別代表飛機處于飛機平飛，上升。使用三個變量x,y,α分別描述飛機的水平位置，垂直位置，以及飛機的仰角度數(shù)。使用常量V,γ表示飛行操作規(guī)則中定義的常量速度和爬升仰角。假設數(shù)據(jù)通信是不可靠的，因此處理器可能會接收不到傳感器傳來的位置參數(shù)，但是在下一次數(shù)據(jù)傳輸中可能接收到數(shù)據(jù)。這種現(xiàn)象以一定概率發(fā)生，并且在下次計算時仍然會以相同的概率觸發(fā)。圖2給出了帶錯誤指令的上升操作模式AADL行為附件。

圖1 現(xiàn)代飛行管理系統(tǒng)多階段示意

Thread thFeaturesPosi:in data port Height:in data port Angle:out data port PropertiesDispatch_protocol=>PeriodicPeriod=>100msEnd th;Thread implementation th.implAnnex Behavior {??ConstantsXp:Base_Types::Unsigned_32yp:Base_Types::Unsigned_32Angle_Climb:Base_Types::Unsigned_32Variablesx:Base_Types::Unsigned_32y:Base_Type::Unsigned_32Ang:Base_Type::Unsigned_32StatesS0:initial stateS1:initial stateS2:stateError:stateS3: complete stateTransient _stateTS0:stateTransitionsS0-[on dispatch]->TS0{Posi?(x);Height?(y)}S1-[x>Xp]->S2{Ang= Angle_Climb;Angle!Ang}S2-[y>yp]->S0{Ang=0;Angle!Ang}Error-[]->S0Transient_TransitionsTS0-[5]->S1TS0-[10]->Error??}End th.impl;

圖2 上升操作模式的AADL行為附件

圖3給出了飛機上升操作模式中物理環(huán)境的AADL模型。

Abstract PlaneFeaturesPosi:out data portHeight:out data portAngle:in data portEnd Plane;Abstract implementation Plane.implAnnex hybrid{??Constants:V:Base_Types::Unsigned_32Variable:x:Base_Types::Unsigned_32y:Base_Type::Unsigned_32Ang:Base_Type::Unsigned_32Behavior:Plane::=!(<{x,y}|x’=V?cos(Ang)y’=V?sin(Ang);@ Posi!(x).Height!(y).Angle?(Ang))??}End Plane.impl

圖3 上升操作模式中的物理信息模型

圖3用混成附件中的微分方程的形式給出了上升操作模式中狀態(tài)變量的變化模型。其中Ang表示飛機仰角，通過接受Angle通道傳來的信息進行調整。X，y分別表示飛機的水平位置和垂直位置信息，通過Posi、Height發(fā)送給行為附件。

4 結束語

信息物理融合系統(tǒng)是由物理組件和計算組件構成的混雜系統(tǒng)。針對帶隨機行為的CPS系統(tǒng)，在進程代數(shù)的基礎上擴展隨機和混成屬性，提出了CPS建模語言HPCCS。HPCCS具有明確的操作語義，可以應用模型檢測或者定理證明[16]技術驗證是否滿足規(guī)約。

AADL是航空系統(tǒng)開發(fā)中廣泛使用的半形式化建模語言，但是AADL在描述物理附件的連續(xù)變化時存在不足。文中擴展了AADL語言，提出混成附件用于對物理行為建模。通過AADL到HPCCS的轉換機制可以將AADL模型自動轉換為形式化語言HPCCS。同時擴展了AADL的行為附件使其能夠描述信息計算系統(tǒng)中存在的隨機行為。該研究為形式化驗證CPS系統(tǒng)打下基礎?；谶@套機制可以將更多形式化方法引入CPS系統(tǒng)相關研究中。