陳　娜, 耿生玲, 李永明, 張勝禮,4

(1.青海師范大學(xué) 計(jì)算機(jī)學(xué)院,青海 西寧810008; 2. 陜西師范大學(xué) 網(wǎng)絡(luò)信息中心,陜西 西安 710069;3. 陜西師范大學(xué) 計(jì)算機(jī)科學(xué)學(xué)院, 陜西 西安 710069;4.興義民族師范學(xué)院 計(jì)算機(jī)科學(xué)系, 貴州 興義 562400)

基于可能性混成自動(dòng)機(jī)的CPS建模方法

陳娜1,2, 耿生玲1, 李永明3, 張勝禮3,4

(1.青海師范大學(xué) 計(jì)算機(jī)學(xué)院,青海 西寧810008; 2. 陜西師范大學(xué) 網(wǎng)絡(luò)信息中心,陜西 西安 710069;3. 陜西師范大學(xué) 計(jì)算機(jī)科學(xué)學(xué)院, 陜西 西安 710069;4.興義民族師范學(xué)院 計(jì)算機(jī)科學(xué)系, 貴州 興義 562400)

摘要:針對(duì)環(huán)境中存在的不確定性因素對(duì)信息物理融合系統(tǒng)的影響，提出一種可能性混成自動(dòng)機(jī)的信息物理融合系統(tǒng)建模方法。該方法以可能性混成自動(dòng)機(jī)為建模工具，通過分析信息物理融合系統(tǒng)的體系結(jié)構(gòu)，討論衡量不確定性的可能性對(duì)信息物理融合系統(tǒng)軟件運(yùn)行時(shí)的動(dòng)態(tài)影響。以汽車速度智能控制系統(tǒng)為例，說明該方法的有效性。

關(guān)鍵詞:信息物理融合系統(tǒng)；可能性混成自動(dòng)機(jī)；可能性CPS；建模

信息物理融合系統(tǒng)(Cyber-Physical Systems, CPS)是一種融合計(jì)算進(jìn)程與物理進(jìn)程復(fù)雜的嵌入式網(wǎng)絡(luò)系統(tǒng)[1]。CPS將物理與計(jì)算進(jìn)程相結(jié)合, 物理設(shè)備通過嵌入式系統(tǒng)和網(wǎng)絡(luò)進(jìn)行監(jiān)測(cè)與控制, 利用反饋機(jī)制相互影響計(jì)算過程與物理過程[2-3], 有效地實(shí)現(xiàn)人與現(xiàn)實(shí)世界的交互控制，以及實(shí)現(xiàn)安全、可靠的反饋控制[4-5]。

CPS由傳感器、執(zhí)行器和控制器等組成, 屬于復(fù)雜性的嵌入式系統(tǒng), 系統(tǒng)中各組件具有自治性、異構(gòu)性、并發(fā)性等特點(diǎn), 且CPS軟件具有開放性[6]。常用的CPS軟件建模方法主要有Simulink/Stateflow和基于UML的方法，由于這些建模方法具有封閉性，目前仍面臨著不確定性建模、管理和優(yōu)化決策控制等方面的挑戰(zhàn)。根據(jù)應(yīng)用的特點(diǎn)與數(shù)據(jù)形式的多樣性，已出現(xiàn)了多種不確定數(shù)據(jù)模型?；诟怕实牟淮_定時(shí)態(tài)數(shù)據(jù)模型，通過分析現(xiàn)有的不確定時(shí)態(tài)信息模型提出概率方法[7]；在概率分布技術(shù)和不確定數(shù)據(jù)聚類方法的基礎(chǔ)上，對(duì)不確定數(shù)據(jù)的概率分布在離散域和連續(xù)域上建模[8]。但是，現(xiàn)實(shí)環(huán)境中仍存在許多問題不能滿足概率模型的可加性，無法用概率模型進(jìn)行建模。

考慮環(huán)境的不確定性對(duì)CPS軟件運(yùn)行動(dòng)態(tài)驗(yàn)證的影響, 本文將可能性概念引入CPS軟件系統(tǒng), 探討不確定性CPS建模與屬性驗(yàn)證的方法。 擬通過一種可能性混成自動(dòng)機(jī)模型用于CPS軟件運(yùn)行動(dòng)態(tài)建模, 并給出該模型屬性驗(yàn)證的描述語法。

1基本概念概述

1.1可能性遷移系統(tǒng)結(jié)構(gòu)

可能性遷移系統(tǒng)結(jié)構(gòu)主要用于解決實(shí)際生活中的非可加性問題，是研究不確定性問題的主要模型。可能性遷移系統(tǒng)結(jié)構(gòu)定義如下。

定義1[9-10]可能性遷移系統(tǒng)結(jié)構(gòu)為五元組M=(S,P,I,AP,L),其中

(1)S是可數(shù)非空狀態(tài)集。

(4)AP是原子命題之集。

(5)L∶S→SAP是標(biāo)簽函數(shù), 即在每個(gè)狀態(tài)下都有一個(gè)賦值(AP的子集)。

若X∈[0,1],分別用∧X和∨X表示X的最小上界和最大下界。

1.2混成自動(dòng)機(jī)

混成自動(dòng)機(jī)結(jié)合了基于狀態(tài)機(jī)的離散控制模型和基于經(jīng)典微分方程表示物理活動(dòng)的連續(xù)變化模型[11]，定義如下。

定義2[12]21-22設(shè)混成自動(dòng)機(jī)為一個(gè)六元組HA=Loc,E,Var,Lab, act, inv。

(1)Loc為控制模式之集。

(2)E為邊的有限之集,表示轉(zhuǎn)換關(guān)系,E的元素e具有形式l,g,a,u,l′,其中的l∈Loc為源位置,g為保衛(wèi)條件,a∈Lab為同步標(biāo)簽,u∈Var×Var為變量的更新關(guān)系，l′為更新后的位置。

(3)Var為實(shí)值變量的有限集,即Var={x1,x2,…,xn},其變量的個(gè)數(shù)也稱為自動(dòng)機(jī)的維度。

(4)Lab為同步標(biāo)簽之集, 同步標(biāo)簽也叫做事件。

(5) act為活動(dòng)標(biāo)記函數(shù), 為混成自動(dòng)機(jī)的每個(gè)位置標(biāo)記一系列的活動(dòng), 活動(dòng)通常用變量對(duì)時(shí)間的微分方程表示。

(6) inv為不變式標(biāo)記函數(shù), 賦予每個(gè)位置一個(gè)不變式。

混成自動(dòng)機(jī)是一個(gè)封閉的智能體, 該系統(tǒng)反映了物理動(dòng)態(tài)與離散變遷之間的相互存在關(guān)系[13-14]。CPS具有離散變遷與連續(xù)動(dòng)態(tài)的行為, 既能描述真實(shí)世界的變化狀況, 又能刻畫系統(tǒng)的狀態(tài)轉(zhuǎn)移關(guān)系。

2可能性CPS軟件擴(kuò)展模型

CPS所處的環(huán)境具有不確定性, 而這些不確定性對(duì)CPS能否正確運(yùn)行在一定程度上起著至關(guān)重要的作用。CPS中各組件并非完全孤立, 它們是相互聯(lián)系的一個(gè)整體。 傳統(tǒng)的嵌入式系統(tǒng)中軟件與硬件高度融合, 但卻具有封閉性, 因此不能單純的使用嵌入式系統(tǒng)軟件的建模方法對(duì)CPS軟件進(jìn)行建模[12]20-21。 本文在嵌入式系統(tǒng)的建模方法基礎(chǔ)上, 將可能性概念引入經(jīng)典的混成自動(dòng)機(jī)表示不確定性, 定義可能性混成自動(dòng)機(jī)網(wǎng)絡(luò)結(jié)構(gòu)模型。

2.1可能性混成自動(dòng)機(jī)

定義3可能性混成自動(dòng)機(jī)H表示為九元組H=L,E,Po,I,Var,Lab, act,inv,C。

(1)L為H中控制模式之集。

(2)E為邊的有限之集,表示轉(zhuǎn)換關(guān)系,E的元素e具有形式l,g,a,u,l′,其中的l∈L為源位置,g為保衛(wèi)條件,a∈Lab為同步標(biāo)簽,u∈Var×Var為變量的更新關(guān)系,l′為更新后的位置。

(3)Po∶L×L→[0,1]是可能性轉(zhuǎn)移函數(shù),且對(duì)?l∈L,都有∨l′∈LPo(l,l′)=1。

(4)I∶L→[0,1]是可能性初始分布函數(shù),且對(duì)?l∈L,都有∨l∈LI(l)=1。

(5)Var為實(shí)值變量的集合,即Var={x1,x2,…,xn},其中變量的個(gè)數(shù)n為H的維度。

(6)Lab為同步標(biāo)簽的集合,稱為H中的事件。

(7) act為活動(dòng)標(biāo)記函數(shù), 為混成自動(dòng)機(jī)的每個(gè)位置標(biāo)記一系列的活動(dòng), 活動(dòng)通常用變量對(duì)時(shí)間的微分方程表示。

(8) inv為不變式標(biāo)記函數(shù), 賦予每個(gè)位置一個(gè)不變式。

(9)C為與H綁定的通信端口的有限集合

C={c1,c2,…,cn}。

此定義中的通信端口起到系統(tǒng)與外界環(huán)境進(jìn)行通信的作用。通信端口的操作方式有兩種,即讀和寫分別用”?”和”!”表示,ci?表示從端口i輸入數(shù)據(jù);ci!表示將數(shù)據(jù)輸出到端口i。 定義為ci={pidi,datai,domi}, 其中pid、dom和data分別為端口i的唯一標(biāo)識(shí)符、傳送的數(shù)據(jù)和數(shù)據(jù)類型。數(shù)據(jù)類型包括integer, boolean, float或用戶自定義。

2.2可能性CPS軟件體系結(jié)構(gòu)模型

2.2.1基于可能性混成自動(dòng)機(jī)的CPS體系結(jié)構(gòu)模型

CPS軟件體系結(jié)構(gòu)由設(shè)備服務(wù)層(感知層和執(zhí)行層)、服務(wù)接口層和高級(jí)應(yīng)用層3層組成, 如圖1所示。服務(wù)接口層的功能體現(xiàn)系統(tǒng)通過與環(huán)境之間的相互影響, 如系統(tǒng)通過與傳感器的交互感知環(huán)境狀態(tài)變化, 及時(shí)實(shí)現(xiàn)對(duì)環(huán)境的監(jiān)控。CPS軟件涉及離散過程和連續(xù)過程的交互, 通過已定義明確的端口與外界環(huán)境進(jìn)行通信并進(jìn)行服務(wù)組合。

圖1　CPS軟件體系結(jié)構(gòu)模型

(1) 設(shè)備類:DC=dcId, Attr, Dom, 其中dcId為設(shè)備類別的唯一標(biāo)識(shí)符; Attr為設(shè)備類的相關(guān)屬性的有限集合; Dom：Attr→DataType表示設(shè)備屬性到數(shù)據(jù)類型的映射關(guān)系, DataType表示傳送的數(shù)據(jù)類型。

(2) 設(shè)備實(shí)體:DE=deId,DC,DH, deId表示設(shè)備實(shí)體的標(biāo)識(shí)符;DC表示與設(shè)備實(shí)體相關(guān)的設(shè)備類;DH表示設(shè)備實(shí)體動(dòng)態(tài)行為的可能性混成自動(dòng)機(jī)。

(3) 原子服務(wù)S=sId, dSet,SH表示, 其中sId是CPS軟件服務(wù)的唯一標(biāo)識(shí)符; dSet為設(shè)備實(shí)體類的集合;SH是描述服務(wù)動(dòng)態(tài)行為的可能性混成自動(dòng)機(jī)。

2.2.2基于可能性混成自動(dòng)機(jī)的CPS體系結(jié)構(gòu)建模

以可能性混成自動(dòng)機(jī)的控制模式進(jìn)行分析,利用可能線性時(shí)序邏輯公式(記為PoLTL)定義可能性CPS軟件模型屬性的形式化描述語言。

定義4可能性 CPS的PoLTL的語構(gòu)定義為

φ∷=ture|a|φ1∧φ2,|φ|Oφ|φ1∪φ2,

其中a∈AP。

設(shè)可能性CPS軟件模型為R,π為模型R的一條執(zhí)行軌跡,φ為屬性描述公式,則用‖φ‖(π)表示R的執(zhí)行軌跡滿足屬性φ。其在R上的語義是Paths(R)的可能性,即‖φ‖R:Paths(R)→[0,1]。π表示整條已知的軌跡,π∈Paths(R)即π=s0s1s2…。用πj表示從第j步開始的軌跡的后綴,即πj=sjsj+1。變量y在π中第j步的值表示為V=(π,j,y)。

可能性CPS軟件模型的執(zhí)行軌跡p可表示為一個(gè)有窮或無窮的序列

s0,t0|→s1,t1|→…|→sn,tn|→…,

其中si=li,vi表示系統(tǒng)的狀態(tài),li表示系統(tǒng)所處的控制模式,vi表示系統(tǒng)當(dāng)前的變量值。ti表示系統(tǒng)在狀態(tài)si停留的時(shí)間。

定義5可能性CPS軟件模型的PoLTL語義可解釋為

‖a‖(πi)=L(si)(a)=y～v?V(π,i,y)～v;

‖φ∧γ‖(πi)=φ∧γ?πi|=φ且πi|=γ;

‖φ‖(πi)=1-‖φ‖(πi)?πi≠φ;

‖Oφ‖(πi)=‖φ‖(πi+1)?π[i+1,…]|=φ;

‖φ∪γ‖(πi)=φ∪γ??t>i,t∈N,s.t.πt|=γ,

且對(duì)于i

在可能性CPS軟件模型R中,無窮路徑表示為π=s0s1s2…∈Sω;有窮路徑表示為π=s0s1…sn(n∈N)。用Paths(R)表示R中無窮路徑之集,Pathsfin(R)表示有窮路徑之集。

R中的狀態(tài)的前驅(qū)Pref表示為

Pref(s)={s′∈S|P(s′,s)>0}

Pref*(s)={s′∈S|s∈Post*(s′)}

后繼Post表示為

Post(s)={s′∈S|P(s,s′)>0};

Post*(s)={s″∈S|?π=s0s1…sk,s0=s,sk=s″,

對(duì)于狀態(tài)集B?S,

3實(shí)例分析

以汽車速度智能控制系統(tǒng)的應(yīng)用為例, 運(yùn)用可能性混成自動(dòng)機(jī)建模方法, 對(duì)汽車速度控制子系統(tǒng)進(jìn)行分析建模, 如圖2所示。用戶給發(fā)動(dòng)機(jī)一個(gè)油門命令, 發(fā)動(dòng)機(jī)得到命令輸出轉(zhuǎn)速給傳動(dòng)器后,將轉(zhuǎn)速轉(zhuǎn)化為驅(qū)動(dòng)汽車運(yùn)動(dòng)的輸出力矩。 傳動(dòng)器需要根據(jù)用戶發(fā)出的油門命令和目前的車速及規(guī)則向傳動(dòng)器發(fā)出控制命令, 使得汽車的運(yùn)行速度能夠改變。

圖2　汽車速度智能控制系統(tǒng)的應(yīng)用場(chǎng)景

在汽車速度智能控制系統(tǒng)中的設(shè)備為執(zhí)行設(shè)備、感知設(shè)備和控制設(shè)備, 各模塊之間通過通信端口與外界環(huán)境進(jìn)行通信。此處的通信端口分別為控制命令、油門和車速。

(1) 執(zhí)行層建模

創(chuàng)建傳動(dòng)器類和傳動(dòng)服務(wù)?？刂泼疃丝诮閏md=(pcmd,c,c→{UP, DOWN, STOP}),

傳動(dòng)器

trans=(Transmission,{gear, cmd,u,n},

{retateSpeed,cmd},{tout},Dom),n為發(fā)動(dòng)機(jī)的轉(zhuǎn)速, gear為加速檔,u為傳動(dòng)器的輸出力矩，傳動(dòng)器到n、gear和u的映射關(guān)系分別表示為

Dom(u)=F+,Dom(n)=F+,Dom(gear)={1,2,3,4}。

傳動(dòng)服務(wù)TransService =(transService, {Trans}, TransH), TransH是描述傳動(dòng)器動(dòng)態(tài)行為的可能性混成自動(dòng)機(jī)，如圖3(a) 所示。

(2) 感知層建模

a) 油門端口和油門感知服務(wù)

油門感知服務(wù)將油門狀態(tài)發(fā)送到油門端口throttle=(pthrottle,x,x|→[0, 1]), 其中x∈[0, 1] 表示油門開起的程度。油門感知服務(wù)ThrottleService=(throttleSer-vice,{Throttle},ThrottleH) , ThrottleH是描述油門傳感器動(dòng)態(tài)行為的可能性混成自動(dòng)機(jī), 如圖3(b)所示。

b) 車速感知服務(wù)

SpeedService=(speedService,{Vehicle},SH),SH是描述車速傳感器動(dòng)態(tài)行為的可能性混成自動(dòng)機(jī),如圖3(c)所示。

(3) 控制層建模

傳動(dòng)器控制服務(wù)TransControllerService=(transControllerService, {Throttle, Trans, Speed},TCSH),TCSH是描述控制器動(dòng)態(tài)行為的可能性混成自動(dòng)機(jī), 如圖3(d) 所示。

考慮環(huán)境不確定性對(duì)汽車速度智能控制系統(tǒng)的影響,以駕駛員對(duì)汽車油門的操作為例, 當(dāng)汽車在道路上行駛時(shí), 路況是不確定的，駕駛員需要根據(jù)路況對(duì)汽車油門進(jìn)行控制。

(4) 駕駛員對(duì)油門操作的不確定性操作建模

(a) 傳動(dòng)服務(wù)

(b) 油門感知服務(wù)

(c) 車速感知服務(wù)

(d) 傳動(dòng)器控制服務(wù)

(e) 駕駛員對(duì)油門的操作

4結(jié)束語

通過對(duì)CPS軟件中的不確定性進(jìn)行研究，定義了可能性混成自動(dòng)機(jī)為形式化建模工具, 以PoLTL作為CPS軟件屬性的形式化描述語言, 描述CPS的體系結(jié)構(gòu)模型及動(dòng)態(tài)行為, 結(jié)合汽車速度智能控制子系統(tǒng)模型，說明該方法的有效性。下一步可能繼續(xù)對(duì)可能性CPS軟件中的屬性進(jìn)行動(dòng)態(tài)驗(yàn)證分析研究。

參考文獻(xiàn)

[1]LEE E . Cyber physical systems: design challenges [C]// Proceedings of 11th IEEE International Symposium on Object Oriented Real-Time Distributed Computing(ISORC),May 5-7,2008, Orlando, F L. Washington, D C: IEEE Xplore, 2008: 363-369. DOI: 10.1109/ISORC.2008.25.

[2]徐洪智, 李仁發(fā), 曾理寧. 基于Ptolemy的信息物理融合系統(tǒng)建模與仿真[J]. 系統(tǒng)仿真學(xué)報(bào), 2014, 26(8): 1633-1638.

[3]尹玲, 陳小紅, 劉靜. 信息物理融合系統(tǒng)的時(shí)間需求性分析[J]. 軟件學(xué)報(bào), 2014,25(2)：400-418. DOI: 10.13328/j.cnki.jos.004540.

[4]封飛, 陳名才, 張廣泉, 等. 基于混成自動(dòng)機(jī)的車聯(lián)網(wǎng)服務(wù)建模方法[J]. 南通大學(xué)學(xué)報(bào)：自然科學(xué)版，2013, 12 (2) : 6-10.

[5]RAJKUMAR R, INSUP L, LUI S. Cyber-physical systems: the next Computing revolution [C]// Proceedings of 47th Design Automation Conference (DAC), June 13-18,2010, Anaheim, C A. New York: ACM, 2010:731-736.

[6]SISTLA A, ZEFRAN M, FENG Y. Runtime monitoring of stochastic cyber-physical systems with hybrid state[C]//2nd International Conference on Runtime Verification (RV 2011). San Francisco, CA, United states: Springer Verlag, 2012:276-293.

[7]任淑霞, 趙政. 基于概率的不確定時(shí)態(tài)數(shù)據(jù)建模與挖掘問題的研究[D]. 天津: 天津大學(xué), 2013: 19-25.

[8]王建榮, 權(quán)義寧. 基于概率分布相似性的不確定數(shù)據(jù)聚類算法研究[D]. 西安: 西安電子科技大學(xué), 2014: 7-13.

[9]李麗君, 李永明. 基于可能性測(cè)度的LTL模型檢測(cè)[D]. 西安：陜西師范大學(xué), 2012: 1-6.

[10]LI L J, LI Y M, Model-checking of Linear-time Properities in Possibilistic Kripke Structure[C]// Quantitative Logic and Soft Computing, Proceedings of the QL&SC 2012. Co. Pet. Ltd: World Scientific, 2012: 287-294.

[11]ALUR R. Formal verification of hybrid systems[C]//Proceedings of the Ninth ACM International Conference on Embed-ded Software(EMSOFT), Oct 9-14, 2011, Taipei. New York : ACM, 2011,12: 273-278.

[12]陳名才, 張廣泉. 基于統(tǒng)計(jì)模型檢測(cè)的CPS軟件可信性驗(yàn)證研究[D]. 蘇州: 蘇州大學(xué), 2014: 20-22.

[13]HENZINGER T. The theory of hybrid automata[C]//Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science(LUCS 96). Washington, D C:IEEE Computer Society, 1996: 278-292.

[14]趙文明, 張敏. 基于時(shí)空I/O混成自動(dòng)機(jī)的物聯(lián)網(wǎng)服務(wù)驗(yàn)證[J]. 科技通報(bào), 2014, 30(5): 95-101.

[責(zé)任編輯：祝劍]

Modeling method of cyber-physical systems based on possibility mixed automaton

CHEN Na1,2,GENG Shengling2,LI Yongming3,ZHANG Shengli3

(1.College of Computer Science, Qinghai Normal University, Xining, Qinghai 810008, China;2. Network Information Center, Shaanxi Normal University, Xi’an, Shanxi 710069, China;3. College of Computer Science, Shaanxi Normal University, Xi’an, Shanxi 710069, China；4. Department of Computer Science, Xingyi Normal University for Nationalities, Xingyi, Guizhou, 562400, China)

Abstract:Due to the influence of uncertainty factors on cyber-physical systems (CPS) in the environment, a typical prototype of CPS architecture and possibility CPS modeling approach based on possibility mixed automaton is given in this paper. The systematic dynamic impaction of non-determined possibility on CPS software is discussed. The case of the vehicle speed control system is presented to show the validity of the modeling method.

Keywords:cyber-physical systems, possibility mixed automaton, possibility CPS, modeling

doi:10.13682/j.issn.2095-6533.2016.01.021

收稿日期：2015-11-10

基金項(xiàng)目：國(guó)家自然科學(xué)基金資助項(xiàng)目 (61261047); 國(guó)家社科基金資助項(xiàng)目 (15XMZ057); 青海省自然科學(xué)基金資助項(xiàng)目 (2014-Z-910, 2015-ZJ-718);貴州省教育廳自然科學(xué)研究重點(diǎn)資助項(xiàng)目(黔教合KY字[2015]408號(hào))

作者簡(jiǎn)介：陳娜(1989-), 女,碩士研究生, 從事計(jì)算機(jī)智能信息處理研究。E-mail: 781698886@qq.com耿生玲(1970-), 女,教授, 博士, CCF會(huì)員(E20033713M), 從事計(jì)算理論, 數(shù)據(jù)挖掘, 控制與決策的研究。E-mail: gengsl@qhnu.edu.cn

中圖分類號(hào)：TP391

文獻(xiàn)標(biāo)識(shí)碼：A

文章編號(hào)：2095-6533(2016)01-0101-05