張福高，曹雪岳

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

0 引 言

AADL是一種支持組件系統(tǒng)建模的語(yǔ)言[1]，用來對(duì)系統(tǒng)的軟、硬件體系結(jié)構(gòu)進(jìn)行建模，并對(duì)系統(tǒng)的功能與非功能性質(zhì)進(jìn)行描述，采用單一模型支持多種分析的方式，從系統(tǒng)的需求分析、設(shè)計(jì)，到系統(tǒng)模型建立、模型驗(yàn)證以及自動(dòng)代碼生成等融合在統(tǒng)一的框架之下[2]。Modelica是一種面向?qū)ο笳Z(yǔ)言，可以應(yīng)用于多領(lǐng)域建模[3-5]。

信息物理系統(tǒng)(CPS)整合了計(jì)算進(jìn)程和物理進(jìn)程[6]，是將計(jì)算(computation)、通信(communication)與控制(control)技術(shù)進(jìn)行有機(jī)和深度融合的下一代智能系統(tǒng)。CPS充分調(diào)度計(jì)算資源與物理資源，合理安排信息物理的融合。CPS追求的是物理世界與計(jì)算過程的深度融合，要實(shí)現(xiàn)二者間的互相通信與控制，要對(duì)CPS進(jìn)行抽象建模比較困難，文獻(xiàn)[7-8]提出了一些集成方法。AADL對(duì)于物理細(xì)節(jié)的建模不如Modelica精確[9]，而在軟件部分建模方面，AADL具有豐富的組件來完成建模工作。為了實(shí)現(xiàn)信息物理系統(tǒng)的建模，完成軟件與硬件的結(jié)合，可以使用Modelica為物理系統(tǒng)模塊進(jìn)行建模，信息系統(tǒng)部分交由AADL組件和行為附件來實(shí)現(xiàn)。

Modelica與AADL不是完全形式化的建模方式，那么很難對(duì)Modelica-AADL模型進(jìn)行形式化驗(yàn)證與分析工作。依據(jù)轉(zhuǎn)換算法進(jìn)行模型轉(zhuǎn)換，再進(jìn)行后續(xù)的形式化驗(yàn)證與分析是一種很好的策略。文獻(xiàn)[10]基于構(gòu)件交互自動(dòng)機(jī)的AADL模型轉(zhuǎn)換方法，之后依據(jù)模型檢測(cè)算法[11]進(jìn)行了驗(yàn)證分析工作。

因此，將Modelica-AADL模型轉(zhuǎn)換成適合的形式化模型很有必要，根據(jù)信息物理融合系統(tǒng)的特性，轉(zhuǎn)換成概率混成自動(dòng)機(jī)[12]，為后續(xù)的驗(yàn)證分析工作奠定基礎(chǔ)。

1 概率擴(kuò)展的Modelica與AADL模型的狀態(tài)

1.1 Modelica中的狀態(tài)

由于Modelica中沒有直接的狀態(tài)轉(zhuǎn)換說明，所以需要進(jìn)行進(jìn)一步的抽象轉(zhuǎn)換。Modelica建模系統(tǒng)中的運(yùn)行與轉(zhuǎn)換關(guān)系主要根據(jù)方程Equation[13]中的定義得出。假設(shè)系統(tǒng)的狀態(tài)集合為Q，系統(tǒng)的當(dāng)前狀態(tài)為s0，那么下面給出Modelica中幾個(gè)重要的Equation下的狀態(tài)劃分規(guī)則。

規(guī)則1：Equation if pred then alt1 else alt2 Equation 存在某一狀態(tài)到兩個(gè)狀態(tài)之間的遷移。

在當(dāng)前狀態(tài)s0下進(jìn)行條件判斷，若滿足條件，則執(zhí)行操作alt1，將之后的狀態(tài)作為新的狀態(tài)s1，若不滿足條件pred，則執(zhí)行操作alt2，將之后的狀態(tài)作為新的狀態(tài)s2。那么s0與狀態(tài)s1,s2就存在著一定的遷移關(guān)系。

規(guī)則2：Equation when pred then op 存在某一狀態(tài)到另外一個(gè)狀態(tài)間的遷移。

在當(dāng)前狀態(tài)s0下進(jìn)行條件判斷，若滿足條件pred，則執(zhí)行操作集合op，這里操作集合op中的操作順序無關(guān)緊要，將之后的狀態(tài)作為新的狀態(tài)s1，那么s0與狀態(tài)s1就存在著一定的遷移關(guān)系。

規(guī)則3：Equation for _indices loop 存在某一狀態(tài)間的循環(huán)。

在當(dāng)前狀態(tài)s0下進(jìn)行循環(huán)，根據(jù)_indices的迭代次數(shù)確定系統(tǒng)在該狀態(tài)下的運(yùn)行，在loop中可以有循環(huán)操作。那么狀態(tài)s0與s0就存在循環(huán)的遷移關(guān)系。

規(guī)則4：Equation connect (component_reference1, component_reference2) 存在某一狀態(tài)到另外一個(gè)狀態(tài)間的遷移。

在component_reference1下的狀態(tài)s0可以遷移到component_reference1下的狀態(tài)s1。在Modelica中connect方程的目的是通過兩個(gè)連接器將兩個(gè)對(duì)象相連。根據(jù)連接關(guān)系，找出連接集合中的內(nèi)連接器與外連接器的對(duì)應(yīng)連接，進(jìn)行連接融合，建立對(duì)應(yīng)連接器內(nèi)對(duì)應(yīng)元素變量的方程關(guān)系。

1.2 Modelica的概率擴(kuò)展

物理組件要根據(jù)物理事件進(jìn)行響應(yīng)，而現(xiàn)實(shí)中的物理事件常常伴有隨機(jī)性。建立隨機(jī)物理系統(tǒng)的模型就變得很有必要。

對(duì)于Modelica的擴(kuò)展有很多實(shí)現(xiàn)[14]，Modelica中的特性有助于將概率因子引入其中。Modelica中的條件集合可以觸發(fā)系統(tǒng)中的離散改變或者事件的發(fā)生。

2 Modelica-AADL建模

2.1 AADL中的狀態(tài)

AADL行為附件是AADL標(biāo)準(zhǔn)核心庫(kù)的擴(kuò)展，提供了描述組件局部功能行為的說明方式。它支持精確描述行為，例如端口通信，計(jì)算，時(shí)間等等。行為附件中具有系統(tǒng)遷移狀態(tài)的描述。

2.2 Modelica與AADL接口設(shè)計(jì)

對(duì)于接口的定義，AADL與Modelica模塊之間具有一定的對(duì)應(yīng)關(guān)系。根據(jù)對(duì)應(yīng)關(guān)系，可以在Modelica中創(chuàng)建一個(gè)AADL工具庫(kù)AADLUnit，也可以在AADL中定義一個(gè)ModelicaPackage，實(shí)現(xiàn)部分，可以利用如xml等形式完成相關(guān)參數(shù)值的注入。

在需要利用接口的時(shí)候，為了在具體的AADL模型中可以描述Modelica中的方程、常量等一些組件變量、參數(shù)的關(guān)系與值傳遞，需要對(duì)AADL引入附加的屬性。

同樣Modelica支持多領(lǐng)域統(tǒng)一建模[15]，利用Modelica中的擴(kuò)展connector組件連接操作，完成參數(shù)變量的傳遞，將AADL與Modelica接口之間的變量關(guān)系以Modelica的形式描述出來。

2.3 Modelica-AADL模型中的狀態(tài)

以AADL狀態(tài)作為基礎(chǔ)，對(duì)Modelica-AADL模型做出如下規(guī)定。

(1)Modelica模型與AADL行為模型中的狀態(tài)可以轉(zhuǎn)化為Modelica-AADL模型中的一般狀態(tài)；

(2)Modelica模型中狀態(tài)的概率遷移可以轉(zhuǎn)換為Modelica-AADL模型中狀態(tài)的概率遷移；

(3)Modelica模型中的傳輸就緒狀態(tài)與AADL行為附件中的狀態(tài)通過接口進(jìn)行關(guān)鍵參數(shù)傳遞時(shí)，可以轉(zhuǎn)換成Modelica-AADL實(shí)例狀態(tài)；

(4)Modelica-AADL實(shí)例狀態(tài)與AADL中的狀態(tài)依然具有遷移關(guān)系，因Modelica-AADL實(shí)例狀態(tài)的一部分屬于AADL狀態(tài)，原先的遷移關(guān)系可以得到保留。

3 Modelica-AADL模型向概率混成自動(dòng)機(jī)的轉(zhuǎn)換

3.1 概率混成自動(dòng)機(jī)

信息物理融合系統(tǒng)(CPS)是物理連續(xù)變化與離散計(jì)算系統(tǒng)相融合的系統(tǒng)架構(gòu)，對(duì)于它的建模，混成自動(dòng)機(jī)是一種比較理想的模型，狀態(tài)上發(fā)生連續(xù)的變換，而離散的變化發(fā)生在狀態(tài)轉(zhuǎn)換之間。為了進(jìn)一步描述CPS中的隨機(jī)成分，將混成自動(dòng)機(jī)擴(kuò)展，引入概率因子，概率混成自動(dòng)機(jī)(PHA)的定義如下：

定義：概率混成自動(dòng)機(jī)可以描述為元組H=(L,X,Σ,E,P,F,I)，其中

(1)L表示有限狀態(tài)集合；

(2)X為變量有限集，可以劃分連續(xù)變量CV與一般變量GV，即變量X=CV∪GV；

(3)∑=∑t∪∑i∪∑o表示傳輸動(dòng)作，輸入動(dòng)作，輸出動(dòng)作的集合；

(4)E?L×Σ×L是變遷的邊集合。其中具體的集合元素形如，包含了保衛(wèi)條件g，同步動(dòng)作a，變量的更新關(guān)系u∈X×X，u包含了必須更新的變量，以及變遷前后保持不變的變量；

(5)P是概率函數(shù)，L×Σ×L→[0,1]，滿足對(duì)于任意l∈L,有∑P(l,α,l')=1,(l,α,l')∈E；

(6)F函數(shù)為狀態(tài)l∈L賦予一個(gè)流條件，F(xiàn)函數(shù)限制了變量的變化率，通常用變量對(duì)時(shí)間的一階導(dǎo)數(shù)方程表示；

(7)I函數(shù)為狀態(tài)l∈L賦予一個(gè)不變式條件，變量需要滿足不變式條件。

3.2 Modelica-AADL模型轉(zhuǎn)換

下面具體描述Modelica-AADL模型(MA模型)向PHA的轉(zhuǎn)換規(guī)則。

(1)Modelica-AADL模型中的狀態(tài)是系統(tǒng)的執(zhí)行狀態(tài)，把它轉(zhuǎn)換到PHA中的狀態(tài)集合L;對(duì)于Modelica-AADL模型中三種類型的狀態(tài)sM|-，sM|sA，-|sA，統(tǒng)一轉(zhuǎn)換成為PHA中的狀態(tài)，構(gòu)成狀態(tài)集合L。

(2)Modelica-AADL模型中的變量，傳輸與端口轉(zhuǎn)換成PHA中的量集合X與動(dòng)作集合Σ。

(3)根據(jù)Modelica-AADL模型中的sM|sA狀態(tài)傳輸?shù)年P(guān)鍵變量的物理連續(xù)變換率轉(zhuǎn)換成為PHA中連續(xù)變量變化率F。

(4)概率混成自動(dòng)機(jī)中的不變條件I根據(jù)具體的系統(tǒng)狀態(tài)限制進(jìn)行轉(zhuǎn)換。

假設(shè)根據(jù)之前的描述，已經(jīng)構(gòu)建了Modelica-AADL模型的概率狀態(tài)遷移ST={S,→,s0},從-|sA類型的初始狀態(tài)s0開始，下面給出模型轉(zhuǎn)換算法的偽代碼。

Function G_PHA(PHA,ST={S,→,s0})

s, v, a，s=s0

While next(s)!=null do

after_s=next(s)

If prob(s,after_s)<1 then

s=BFS(S,→,s) continue

End

v=getData(after_s)

a=getEvent(s,after_s)

L=L∪(after_s),X=X∪v,∑=∑∪a

E=E∪{(s,a,after_s)},P(s,after_s)=1

End

Return PHA(L,X,Σ,E,P,F)

Function BFS(S,→,root)

Q, Visited, s, tail, v, a

Visited=Visited∪root Enque(Q,root)

Whileempty(Q)==false do

s=Deque(Q) after_s=next(s)

Ifafter_s=null then continue

End

While after_s!=null do

v=getData(after_s)

a=getEvent(s,after_s)

Ifafter_s?Visitedthen

L=L∪(after_s),E=E∪{(s,a,after_s)},P(s,after_s)=prob(s,after_s)

Visited=Visited∪after_s

Enque(Q,after_s)

after_s=next(s)

Else

E=E∪{(s,a,after_s)},P(s,after_s)=prob(s,after_s)

F(v,after_s)=getEquation(v,after_s)

tail=after_s

End

X=X∪v,∑=∑∪a,

End

End

Return tail

next(s)函數(shù)返回s的下一個(gè)狀態(tài)的狀態(tài)列表的第一個(gè)狀態(tài)(因?yàn)楦怕兽D(zhuǎn)移的存在，s的下一個(gè)狀態(tài)可能會(huì)有多個(gè))。next函數(shù)內(nèi)置一個(gè)指針再次調(diào)用next將返回狀態(tài)列表的后一個(gè)狀態(tài)，直到狀態(tài)列表遍歷完畢，指針重置指向第一個(gè)位置。

prob(s1,s2)函數(shù)返回狀態(tài)之間的遷移概率，不涉及概率的狀態(tài)遷移，將概率看作1。

getEquation(s)函數(shù)返回sM|sA類型狀態(tài)s中傳遞的關(guān)鍵連續(xù)物理變量的變化函數(shù)。

getData(s)函數(shù)返回狀態(tài)中的變量并將其歸類到CV與GV，包括CV包含modelica物理連續(xù)變量，GV包含AADL行為狀態(tài)的數(shù)據(jù)端口以及狀態(tài)變量。

getEvent(s1,s2)返回狀態(tài)間的動(dòng)作并將其歸類到∑i，∑o和∑t，∑i,∑o包括了AADL行為狀態(tài)的事件端口，∑t包括了Modelica_AADL接口的傳輸動(dòng)作。

4 結(jié)束語(yǔ)

信息物理融合系統(tǒng)的建模與驗(yàn)證是一項(xiàng)復(fù)雜且十分困難的工作。Modelica與AADL是兩種優(yōu)秀的建模語(yǔ)言，對(duì)于CPS的建模工作交由這兩種建模方式組合處理是一個(gè)可取的策略。將物理系統(tǒng)的建模工作交給Modelica處理，將信息計(jì)算系統(tǒng)的建模工作交給AADL處理，這種混合建模方式可以充分利用二者的優(yōu)勢(shì)。Modelica與AADL相結(jié)合的重點(diǎn)就是如何建立它們的聯(lián)系，文中完成了Modelica-AADL接口的設(shè)計(jì)，向Modelica中添加了概率擴(kuò)展用以描述物理系統(tǒng)中的隨機(jī)性，抽象出了Modelica模型中原來并不存在的狀態(tài)，進(jìn)而結(jié)合AADL行為附件的系統(tǒng)狀態(tài)，定義了Modelica-AADL模型中的系統(tǒng)狀態(tài)。之后制定了相關(guān)規(guī)則，將Modelica-AADL模型轉(zhuǎn)換成了概率混成自動(dòng)機(jī)模型，為后續(xù)的形式化分析與驗(yàn)證工作奠定了基礎(chǔ)。