曹雪岳，曹子寧，卜星晨

(南京航空航天大學(xué) 計算機(jī)科學(xué)與技術(shù)學(xué)院，江蘇 南京 211106)

0 引 言

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

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

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

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

1 混成隨機(jī)進(jìn)程代數(shù)-HPCCS

進(jìn)程代數(shù)最早用來刻畫通信系統(tǒng)的行為，可以描述系統(tǒng)的并發(fā)特性。文中在CCS的基礎(chǔ)上提出一種用于CPS系統(tǒng)建模的進(jìn)程代數(shù)HPCCS。HPCCS能夠描述CPS系統(tǒng)的連續(xù)變化，還可以描述CPS系統(tǒng)中存在的概率行為。本節(jié)將詳細(xì)給出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:=ε//空進(jìn)程

|a.P//離散動作

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

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

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

|c?d>>P//流動作，?P表示P進(jìn)程可以中斷流動作

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

|P[A] //隱藏算子

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

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

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

在定義的進(jìn)程算子的基礎(chǔ)上，通過遞歸定義引入幾個常用算子。首先同步并發(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后可以定義進(jìn)程間順序組合：

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

接下來通過水箱系統(tǒng)的例子說明HPCCS的建模能力。水箱系統(tǒng)[13]是由水箱和控制器組成，控制器通過傳感器獲取水位，根據(jù)設(shè)定的水位閾值決定是否關(guān)閉進(jìn)水系統(tǒng)。當(dāng)進(jìn)水系統(tǒng)關(guān)閉時水位由于漏水開始下降。文中在控制器部分引入錯誤，當(dāng)水位低于最低值的時候由于控制器故障可能不會打開注水閥門，該故障隨機(jī)出現(xiàn)，并且出現(xiàn)后可以自動修復(fù)，故障率為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的語義是通過結(jié)構(gòu)化操作語義[14]規(guī)則描述。目前形式化描述語義主要有：操作語義、指稱語義、公理語義和代數(shù)語義。操作語義是通過抽象的方法描述語言中每個基本算子的執(zhí)行效果，避免描述的語言依賴于實現(xiàn)的具體計算機(jī)系統(tǒng)，一般使用狀態(tài)遷移系統(tǒng)描述。該方法的優(yōu)點在于具有直觀的表現(xiàn)形式。

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

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

給定一個HPCCS進(jìn)程S，可以得到S對應(yīng)的標(biāo)號遷移系統(tǒng)T(P)=，構(gòu)造標(biāo)號遷移系統(tǒng)的過程如下：

(1)狀態(tài)集Q=subp(P)∪{ε}×V(S)，其中subp(P)表示進(jìn)程P的所有子進(jìn)程組成的集合，例如P:=[t|t+=0]>>(?[t>3]>>P)，subp(P')={S,[t>3]>>P,,ε}∪subp(P'),ε表示終止進(jìn)程。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表示開始時的進(jìn)程，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)上的不確定選擇。文中在行為附件的基礎(chǔ)上引入概率選擇的狀態(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。提出擴(kuò)展隨機(jī)選擇的行為附件規(guī)范，定義如下：

定義4：帶隨機(jī)選擇的行為附件。

帶隨機(jī)選擇行為的行為附件，隨機(jī)選擇狀態(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è)備間的數(shù)據(jù)通信。混成附件作為AADL設(shè)備組件的注解，對傳感器和執(zhí)行器的連續(xù)行為建?；蛘咦鳛槌橄蠼M件實現(xiàn)。混成附件規(guī)范由三個部分組成：變量，組件的通信接口集合，HPCCS進(jìn)程描述的行為集合。

定義5：混成附件。

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

HA::=(Variables，Channels，Proc)

其中Variables表示系統(tǒng)中的變量，Proc表示由HPCCS表示的進(jìn)程組成的集合，用于對物理設(shè)備建模。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的轉(zhuǎn)換規(guī)則

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

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

(2)狀態(tài)集合中的狀態(tài)分別對應(yīng)一個進(jìn)程變量。

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

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

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

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

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

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

考慮飛機(jī)上升時的操作。首先飛機(jī)以平飛的模式到達(dá)指定水平位置，控制器驅(qū)動飛機(jī)進(jìn)入上升狀態(tài)，開始向上爬升。當(dāng)達(dá)到指定高度后，控制器驅(qū)動飛機(jī)進(jìn)入水平飛行狀態(tài)。因此上升操作模式可以抽象出三個狀態(tài)，s1,s2分別代表飛機(jī)處于飛機(jī)平飛，上升。使用三個變量x,y,α分別描述飛機(jī)的水平位置，垂直位置，以及飛機(jī)的仰角度數(shù)。使用常量V,γ表示飛行操作規(guī)則中定義的常量速度和爬升仰角。假設(shè)數(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給出了飛機(jī)上升操作模式中物理環(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表示飛機(jī)仰角，通過接受Angle通道傳來的信息進(jìn)行調(diào)整。X，y分別表示飛機(jī)的水平位置和垂直位置信息，通過Posi、Height發(fā)送給行為附件。

4 結(jié)束語

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

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