基于可能性時(shí)空混成自動(dòng)機(jī)的CPS軟件建模

彭姣+耿生玲+童英華+宮海彥

摘 要： 信息物理融合系統(tǒng)（CPS）對(duì)復(fù)雜系統(tǒng)的建模與驗(yàn)證是當(dāng)前控制研究領(lǐng)域的一個(gè)熱點(diǎn)問題。考慮不確定環(huán)境因素對(duì)CPS系統(tǒng)的影響，結(jié)合可能性測(cè)度與時(shí)空模型，給出一種可能性時(shí)空混成自動(dòng)機(jī)的信息物理融合系統(tǒng)的建模方法。以時(shí)空混成自動(dòng)機(jī)為建模工具，通過分析CPS的體系結(jié)構(gòu)，討論衡量不確定性的可能性對(duì)CPS軟件運(yùn)行時(shí)的時(shí)空動(dòng)態(tài)影響，給出一個(gè)可能性時(shí)空CPS系統(tǒng)架構(gòu)。通過理論證明和實(shí)例分析在不確定環(huán)境下可能性時(shí)空混成自動(dòng)機(jī)為CPS軟件系統(tǒng)建模的可行性。

關(guān)鍵詞： CPS； 不確定性； 可能性時(shí)空混成自動(dòng)機(jī)； 控制系統(tǒng)； 建模； 屬性驗(yàn)證

中圖分類號(hào)： TN876?34； TP391 文獻(xiàn)標(biāo)識(shí)碼： A 文章編號(hào)： 1004?373X（2018）05?0173?05

Abstract： The complex system modeling and validation by means of the cyber?physical system （CPS） is a hotspot issue of the current control study field. Considering the influence of the uncertain environment on CPS， the possibility measurement and spatio?temporal model are combined to give a modeling method of CPS based on possibility spatio?temporal hybrid automata. Taking the spatio?temporal hybrid automata as the modeling tool， analyzing the architecture of the CPS， and discussing the influence of nondeterminacy′s possibility on the spatio?temporal dynamic behavior when the CPS software is running， an architecture of the possibility spatio?temporal CPS is given. The theory verification and instance analysis results show that the CPS software modeling based on possibility spatio?temporal hybrid automata is feasible in uncertain environment.

Keywords： cyber?physical system； indeterminacy； possibility spatio?temporal hybrid automata； control system； modeling； property verification

0 引 言

信息物理融合系統(tǒng)（Cyber?Physical Systems，CPS）是一種融合計(jì)算進(jìn)程與物理進(jìn)程的復(fù)雜嵌入式網(wǎng)絡(luò)系統(tǒng)[1]，并且已經(jīng)在很多領(lǐng)域廣泛應(yīng)用。實(shí)現(xiàn)的反饋控制既安全又可靠，還可以有效實(shí)現(xiàn)人與現(xiàn)實(shí)世界的交互。該領(lǐng)域研究的一個(gè)熱點(diǎn)問題是CPS系統(tǒng)的建模及其驗(yàn)證。CPS體系中各組件具備自治性、異構(gòu)性、并發(fā)性等特性，相對(duì)于傳統(tǒng)的嵌入式系統(tǒng)，CPS軟件與硬件高度融合，各組件并非完全孤立，而是彼此關(guān)聯(lián)的一個(gè)整體，擁有離散與連續(xù)動(dòng)態(tài)變化的行為，使得利用傳統(tǒng)方式對(duì)CPS軟件建模具有挑戰(zhàn)性?；斐勺詣?dòng)機(jī)既能描述真實(shí)世界的變化狀況，又能刻畫系統(tǒng)的狀態(tài)轉(zhuǎn)移關(guān)系，因此該模型成為研究CPS系統(tǒng)的重要基礎(chǔ)[2?5]。更多地，文獻(xiàn)[6]提出一種異構(gòu)模型，引入行為關(guān)系以表達(dá)系統(tǒng)之間不同的模型語(yǔ)義，實(shí)現(xiàn)對(duì)系統(tǒng)屬性的形式化驗(yàn)證；文獻(xiàn)[7]提出具有位置驅(qū)動(dòng)特點(diǎn)的時(shí)空自動(dòng)機(jī)；文獻(xiàn)[8]根據(jù)混成自動(dòng)機(jī)與HP模型之間的轉(zhuǎn)換規(guī)則提出一種CPS軟件模型與屬性驗(yàn)證框架。這些都是經(jīng)典的一些CPS軟件模型與屬性驗(yàn)證框架。

在實(shí)際系統(tǒng)中，由于CPS所處的環(huán)境具有不確定性，而這些不確定性對(duì)CPS是否能正確運(yùn)行在一定程度上起著至關(guān)重要的作用。通常經(jīng)典的模型和檢測(cè)方法不能處理實(shí)際系統(tǒng)中的這些不確定的建模與屬性驗(yàn)證問題?？赡苄詼y(cè)度是模糊集理論的一個(gè)分支，是對(duì)概率測(cè)度的推廣，可能性測(cè)度不滿足可加性。文獻(xiàn)[9?11]將可能性測(cè)度模糊數(shù)學(xué)與模型檢測(cè)技術(shù)相結(jié)合，提出基于可能性測(cè)度的模型檢測(cè)方法。為復(fù)雜系統(tǒng)的不確定性驗(yàn)證提供了較好的理論基礎(chǔ)。

本文考慮不確定環(huán)境對(duì)CPS系統(tǒng)的影響，提出一種基于可能性時(shí)空混成自動(dòng)機(jī)模型，給出CPS系統(tǒng)建模和可能性時(shí)空CPS的描述語(yǔ)言。從理論和實(shí)例兩方面驗(yàn)證基于該模型為不確定環(huán)境下CPS系統(tǒng)建模和屬性驗(yàn)證度量方法的有效性，從而為復(fù)雜CPS系統(tǒng)的智能控制與優(yōu)化提供理論依據(jù)。

1 基本概念

定義1[12]：設(shè)是一個(gè)非空集合，是由的子集構(gòu)成的集合（包含空集），且對(duì)集合的補(bǔ)運(yùn)算和可數(shù)任意并運(yùn)算封閉，則稱是一個(gè)代數(shù)，為可測(cè)空間。映射表示代數(shù)上的可能性測(cè)度，且滿足以下性質(zhì)：

定義2[13]：混成自動(dòng)機(jī)為六元組：

其中：Loc為控制模式的集合；為邊的有限集合，即表示轉(zhuǎn)換關(guān)系。對(duì)于其中為源位置，為目標(biāo)位置，為保衛(wèi)條件，為同步標(biāo)簽，為變量的更新關(guān)系；為實(shí)值變量的有限集，即稱為自動(dòng)機(jī)的維度；Lab為同步標(biāo)簽的集合，同步標(biāo)簽也叫做事件；Act為活動(dòng)標(biāo)記函數(shù)，以此來表示混成自動(dòng)機(jī)每個(gè)位置標(biāo)識(shí)的一系列活動(dòng)，通常用變量對(duì)時(shí)間的微分方程表示；Inv為不變式標(biāo)記函數(shù)，賦予每個(gè)位置一個(gè)不變式。endprint

CPS具有離散與連續(xù)動(dòng)態(tài)變化的行為，它既能描述真實(shí)世界的變化狀況，又能刻畫系統(tǒng)的狀態(tài)轉(zhuǎn)移關(guān)系。所以，混成自動(dòng)機(jī)成為研究CPS系統(tǒng)至關(guān)重要的基礎(chǔ)。

2 可能性時(shí)空混成自動(dòng)機(jī)

在實(shí)際系統(tǒng)中，由于環(huán)境的不確定性對(duì)CPS正確運(yùn)行在一定程度上產(chǎn)生一定影響。因此，在研究混成自動(dòng)機(jī)的基礎(chǔ)上，本文引入可能性測(cè)度和時(shí)空邏輯，給出具有描述位置或者空間行為信息的不確定性CPS軟件的建模。

定義3：可能性時(shí)空混成自動(dòng)機(jī)用八元組表示，其中：

1）是一個(gè)離散狀態(tài)集或者控制模式集；

2）是可能性時(shí)空混成自動(dòng)機(jī)的連續(xù)狀態(tài)空間，通常情況下，是一個(gè)?維分支；

3）是標(biāo)簽有限集，用來標(biāo)記狀態(tài)轉(zhuǎn)換的邊的標(biāo)簽集合；

4）是變量的集合，這些變量存在于每個(gè)模式中，并由所在的模式惟一決定。這個(gè)變量包含離散變量的集合dVar、 連續(xù)變量的集合cVar、 時(shí)鐘變量的集合ckVar和空間變量集合sVar；

5）是控制圖中邊的集合，稱為遷移。每個(gè)邊可以定義為四元組： ，其中： ，是可能性轉(zhuǎn)移函數(shù)； ，是警衛(wèi)條件，它可以描述從跳轉(zhuǎn)的條件；是遷移發(fā)生時(shí)將要發(fā)生的動(dòng)作。對(duì)于，，都有；

6） Inv是模式中必須滿足的條件，稱為不變式。具體來說，就是每個(gè)模式對(duì)應(yīng)的一個(gè)子集；

7） Act表示模式的標(biāo)記函數(shù)，它表達(dá)為一些微分方程的合取式。每個(gè)模式都對(duì)應(yīng)一個(gè)模式活動(dòng)Act，它描述在模式中連續(xù)變量隨時(shí)間變化的情況；

8） 是可能性初始分布函數(shù)，對(duì)于，都有。

在以上可能性時(shí)空混成自動(dòng)機(jī)的定義中，對(duì)于 當(dāng)滿足條件，一個(gè)從的遷移就會(huì)發(fā)生，同時(shí)，離散變量跳轉(zhuǎn)到一個(gè)新值記為對(duì)于有：

表明一個(gè)遷移有效，當(dāng)且僅當(dāng)滿足如下條件：

下面為列車控制系統(tǒng)的一個(gè)制動(dòng)行為可能性時(shí)空混成自動(dòng)機(jī)模型實(shí)例，如圖1所示。

用表示第一輛車的安全距離，表示第一輛車的緊急制動(dòng)距離，表示第二輛車的安全距離，表示第二輛車的緊急制動(dòng)距離，根據(jù)關(guān)系知，表示相離，表示相交。其模型為其中：

{Initinal，BarkingNoRequired，Barkingrequird，Initinal1，EmergeBarkingRequired，NormalBarkingRequired，Initinal2，Wating，Barking}；

在可能性時(shí)空混成自動(dòng)機(jī)模型的遷移系統(tǒng)中，為了簡(jiǎn)便，系統(tǒng)的時(shí)空狀態(tài)表示為，其中為標(biāo)簽，表示當(dāng)前的狀態(tài)， 表示其控制模式，表示在狀態(tài)停留的時(shí)間，表示在狀態(tài)時(shí)的位置，表示對(duì)應(yīng)位置的速度。

3 可能性時(shí)空CPS軟件模型

基于可能性時(shí)空混成自動(dòng)機(jī)的CPS結(jié)構(gòu)稱為可能性時(shí)空CPS模型，其體系結(jié)構(gòu)可由三層組成，即設(shè)備服務(wù)層、服務(wù)接口層和高級(jí)應(yīng)用層，如圖2所示。服務(wù)接口層的功能體現(xiàn)系統(tǒng)與環(huán)境之間相互影響，CPS軟件涉及離散過程和連續(xù)過程的交互，通過已定義的明確端口與外界進(jìn)行通信等。

1） 設(shè)備類：DC=，其中Id為設(shè)備類別的惟一標(biāo)識(shí)符；Att為設(shè)備類的相關(guān)屬性的有限集合； Dom：Att→DataType表示設(shè)備屬性到數(shù)據(jù)類型的一個(gè)映射，DataType表示傳送數(shù)據(jù)的類型，如integer，boolean，float和用戶自定義的數(shù)據(jù)類型。

2） 設(shè)備實(shí)體：DE=，其中DId是設(shè)備實(shí)體的惟一標(biāo)識(shí)符；DC是設(shè)備實(shí)體所屬的設(shè)備類； DH是描述設(shè)備實(shí)體動(dòng)態(tài)行為的可能性時(shí)空混成自動(dòng)機(jī)。

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

可能性時(shí)空CPS模型的遷移系統(tǒng)中，無(wú)窮路徑表示為：有窮路徑表示為：。用Paths表示中無(wú)窮路徑的集合，Pathsfin表示有窮路徑的集合。

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

后繼Post表示為：

而對(duì)于如果定義可得擴(kuò)張映射， 則稱映射Po是上的時(shí)空可能性測(cè)度。其中，表示狀態(tài)的前驅(qū)狀態(tài)。

定理1：設(shè)為可能性時(shí)空CPS模型，則稱為上由生成的代數(shù)。

定理2：設(shè)是可能性時(shí)空CPS模型，則從初始狀態(tài)出發(fā)的路徑的可能性為：

4 實(shí)例分析

以ETCS兩輛列車智能控制CPS系統(tǒng)的應(yīng)用場(chǎng)景為例，考慮環(huán)境的不確定性對(duì)列車運(yùn)行時(shí)速度和距離的影響。如圖3所示，兩輛列車在列車自我防護(hù)（ATP）子系統(tǒng)監(jiān)控下行駛，從而避免列車超速，防止列車碰撞。運(yùn)用可能性時(shí)空混成自動(dòng)機(jī)建模方法對(duì)ATP子系統(tǒng)進(jìn)行分析建模。

1） 執(zhí)行層建模

創(chuàng)建ATP類、制動(dòng)類和ATP服務(wù)、制動(dòng)服務(wù)。

ATP類，其中，sensor是傳感器，Cmd是命令端口。

ATP服務(wù)：ATPService=（ATPService，{ATP}，AtpHA），AtpHA是描述監(jiān)測(cè)距離服務(wù)或者速度監(jiān)測(cè)服務(wù)的可能性時(shí)空混成自動(dòng)機(jī)，如圖4a），圖4b）所示。

2） 感知層建模

速度感知服務(wù)：SpeedService=（speedService，{Trains}，SH），SH是描述列車速度動(dòng)態(tài)變化的可能性時(shí)空混成自動(dòng)機(jī)，如圖4c）所示。

距離感知服務(wù)：DistService=（distService，{Trains}，SSH），SSH是描述列車距離動(dòng)態(tài)變化的可能性時(shí)空混成自動(dòng)機(jī)，如圖4d）所示。

3） 控制層建模

ATP控制服務(wù)：ContrService=（contrService，{ATP，Train，Speed}，Cmd，TCSH），TCSH是描述ATP控制行為的可能性時(shí)空混成自動(dòng)機(jī)，如圖4e）所示。

5 結(jié) 語(yǔ)

基于CPS軟件的不確定性，結(jié)合可能混成自動(dòng)機(jī)模型給出軟件定義CPS形式的時(shí)空建模工具和形式化描述語(yǔ)言，描述CPS的體系結(jié)構(gòu)模型及動(dòng)態(tài)行為，利用列車控制系統(tǒng)模型闡明該方法的有效性。下一步將繼續(xù)對(duì)可能性CPS軟件屬性進(jìn)行動(dòng)態(tài)驗(yàn)證分析和不確定性時(shí)空模型下的智能控制方法進(jìn)行研究，并將其應(yīng)用于機(jī)器人工業(yè)、汽車電子、智能電網(wǎng)、智能家居、醫(yī)療衛(wèi)生等應(yīng)用領(lǐng)域，為復(fù)雜CPS系統(tǒng)的智能控制與優(yōu)化提供更多理論依據(jù)。

參考文獻(xiàn)

[1] LEE E A. Cyber physical system： designer challenges [C]// Proceeding of the 11th IEEE International Symposium on Object Oriented Computing. Orlando： IEEE， 2008： 363?369.

[2] THOMAS A H. The theory of hybrid automata [C]// Proceedings of 1996 LICS. [S.l.： s.n.]， 1996： 278?292.

[3] RAJEEV A， COSTAS C， THOMAS A H， et al. Hybrid automata： an algorithmic approach to the specification and verification of hybrid system [J]. Hybrid systems， 1993， 736： 209?229.

[4] THOMAS A H， PETER W K， PURI A， et al. What′s deci?dable about hybrid automata [J]. Journal of computer and system sciences， 1998， 57（1）： 373?382.

[5] FENG Y， YANG Xia， SHEN Zhaoxiang， et al. Modeling computation entity of CPS based on dynamic behavior [J]. Journal of system simulation， 2016， 28（5）： 1003?1016.

[6] AKSHAY R， BRUCE H K. Heterogeneous verification of cyber?physical system using behavior relation [C]// Proceedings of the 15th ACM International Conference on Hybrid System： Computation and Control. [S.l.： s.n.]， 2012： 35?44.

[7] ZHAO Wenming， CHEN Yixiang， ZHANG Min. Modeling and verification of CPS based on spatial hybrid automata [J]. Bulletin of science and technology， 2015， 31（1）： 94?99.

[8] TIAN Mingfu， ZHANG Xingshe， LIN Jialin， et al. Behavior modeling and attribute validation of cyber?physical system （CPS） based on hybrid automata [J]. Journal of Air Force Engineering University （natural science edition）， 2016， 17（3）： 40?44.

[9] LI Lijun， LI Yongming. Model?checking of linear?time properties in possibilistic Kripke structure [C]// Proceedings of the 2012 QL&SC. [S.l.]： World Scientific， 2012： 2870?2894.

[10] 李永明.可能LTL模型檢測(cè)的兩種方法[J].陜西師范大學(xué)學(xué)報(bào)（自然科學(xué)版），2014，42 （6）：21?25.

LI Yongming. Two methods for possibilistic linear temporal logic model checking [J]. Journal of Shaanxi Normal University （natural science edition）， 2014， 42（6）： 21?25.

[11] LI Yongming， LI Lijun. Model checking of linear?time properties based on possibility measure [J]. IEEE transactions on fuzzy systems， 2013， 21（5）： 842?854.

[12] 李麗君.基于可能性測(cè)度的LTL模型檢測(cè)[D].西安：陜西師范大學(xué)，2012.

LI Lijun. LTL modeling checking based on possibility measure [D]. Xian： Shaanxi Normal University， 2012.

[13] 張建寧.基于混成自動(dòng)機(jī)的CPS構(gòu)建服務(wù)組合建模與驗(yàn)證[D].蘇州：蘇州大學(xué)，2014.

ZHANG Jianning. Modeling verifying of CPS component service composition based on hybrid automata [D]. Suzhou： Soochow University， 2014.endprint