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

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

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

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

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

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

1 基本概念

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

定義2[13]：混成自動機為六元組：

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

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

2 可能性時空混成自動機

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

定義3：可能性時空混成自動機用八元組表示，其中：

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

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

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

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

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

6） Inv是模式中必須滿足的條件，稱為不變式。具體來說，就是每個模式對應的一個子集；

7） Act表示模式的標記函數(shù)，它表達為一些微分方程的合取式。每個模式都對應一個模式活動Act，它描述在模式中連續(xù)變量隨時間變化的情況；

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

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

表明一個遷移有效，當且僅當滿足如下條件：

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

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

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

在可能性時空混成自動機模型的遷移系統(tǒng)中，為了簡便，系統(tǒng)的時空狀態(tài)表示為，其中為標簽，表示當前的狀態(tài)， 表示其控制模式，表示在狀態(tài)停留的時間，表示在狀態(tài)時的位置，表示對應位置的速度。

3 可能性時空CPS軟件模型

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

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

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

3） 原子服務，其中sId是CPS軟件服務的惟一標識符；dSet為設備實體類的集合；SH是描述服務動態(tài)行為的可能性時空混成自動機。

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

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

后繼Post表示為：

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

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

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

4 實例分析

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

1） 執(zhí)行層建模

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

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

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

2） 感知層建模

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

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

3） 控制層建模

ATP控制服務：ContrService=（contrService，{ATP，Train，Speed}，Cmd，TCSH），TCSH是描述ATP控制行為的可能性時空混成自動機，如圖4e）所示。

5 結(jié) 語

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

參考文獻

[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模型檢測的兩種方法[J].陜西師范大學學報（自然科學版），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] 李麗君.基于可能性測度的LTL模型檢測[D].西安：陜西師范大學，2012.

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

[13] 張建寧.基于混成自動機的CPS構(gòu)建服務組合建模與驗證[D].蘇州：蘇州大學，2014.

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