王 鵬 向 陽 宗宇偉 張 騏

①(同濟大學電子與信息工程學院 上海 201804)

②(上海計算機軟件技術開發(fā)中心 上海 201112)

③(神華和利時信息技術有限公司 北京 100011)

1 引言

信息物理融合系統(tǒng)(Cyber Physical System,CPS)是近幾年出現(xiàn)的一個新概念。CPS[1,2]是一種計算、通信與控制融合的新型復雜嵌入式系統(tǒng)，由計算單元、控制單元、執(zhí)行器節(jié)點和傳感器節(jié)點構成。系統(tǒng)中計算過程和物理過程在開放環(huán)境下持續(xù)交互、深度融合與相互作用，一體化地實現(xiàn)開放嵌入式計算、網絡化實時通信與遠程精確控制等先進功能。CPS已引起許多國家學術界和工業(yè)界的高度重視。美國總統(tǒng)科學與技術顧問委員會(PCAST)于2007年7月把CPS作為網絡與信息技術領域的第一優(yōu)先發(fā)展方向，由此引起美國多個政府機構、高校和企業(yè)數億美元以及大量人力物力的投入。歐盟FP7的Artemis項目(2008-2017)計劃投入27億歐元開展嵌入式計算與CPS相關技術的研發(fā)。日本、韓國等也已在近年先后設立了針對 CPS的研究計劃。我國也相當重視CPS的研究工作，國家高技術研究發(fā)展計劃(863計劃)課題“面向信息-物理融合的系統(tǒng)平臺”已于2011年底正式啟動。

當構成CPS的組件升級或者發(fā)生故障時，需要被新的組件替換，替換后的系統(tǒng)能否正常運行是一個非常值得研究的問題。要從理論上判定CPS組件的可替換性，CPS體系結構是首先要解決的問題。目前國內外在這方面的研究還處于起步階段，文獻[3]從CPS特征角度提出一種體系結構原型，但并未詳細介紹如何實現(xiàn)。文獻[4]提出一種多模式復合框架，但不適用于擁有多個并發(fā)處理單元的CPS。文獻[5]提出一種面向服務的中間件模型，偏重于從中間件角度設計CPS的體系結構。本文提出一種面向服務的CPS體系結構，把CPS中的各種不同操作系統(tǒng)、中間件、編程語言的異構軟硬件資源結合在一起封裝成服務，將 CPS組件的可替換性等價為CPS服務的可替換性，便于進行統(tǒng)一的形式化分析與判定。針對CPS領域的形式化驗證方法，已有眾多研究成果[6]，包括基于Petri網[7]、有限狀態(tài)機[8]、進程代數[9]等。Petri網和有限狀態(tài)機所采用的圖形方式較為直觀，但當交互過程變得復雜時，這種圖形刻畫的方式容易出現(xiàn)狀態(tài)空間爆炸，計算、驗證和判定的復雜度也隨即增加。進程代數中的π-演算專門用于描述移動進程和結構不斷變化，可自行重配置的網絡，采用π-演算是web服務可替換性判定的一種常見方法[10]。但是，與傳統(tǒng)的web軟件相比，CPS包含傳感器、控制器等物理部件，受到時間和空間條件的約束，具有時空特性，而經典π-演算缺乏支持時空特性的語法和語義。本文對經典π-演算進行擴充，引入時間和空間算子，提出時空π-演算理論，對CPS服務進行形式化建模。從服務可替換性和兼容性的關系[11,12]入手，基于π-演算的弱互模擬理論，提出一種CPS服務可替換性判定方法，從而在設計階段就能發(fā)現(xiàn)CPS組件的替換是否正確，避免后期付出更大的代價，減少不必要的開銷。

本文第2節(jié)給出CPS服務的定義；第3節(jié)提出時空π-演算理論，進而對 CPS服務形式化建模，結合服務可替換性和兼容性的關系，給出CPS服務可替換性判定方法；第4節(jié)通過電子圍欄案例，說明如何判定CPS組件的可替換性；最后是結束語。

2 CPS 服務

本節(jié)采用面向服務[13]的體系結構設計分布式、開放性的CPS，把復雜的CPS看作一系列封裝好的CPS服務按照一定的業(yè)務邏輯和業(yè)務流程組合而成。該體系結構框架如圖1所示，框架將CPS系統(tǒng)分為4層：應用層、業(yè)務流程層、服務抽象層和服務實現(xiàn)層。CPS服務包括服務實現(xiàn)和服務抽象兩部分。因本文重點在CPS組件的可替換性研究，以下僅介紹 CPS服務，其余分層的詳細構成可聯(lián)系作者。

圖1 面向服務的CPS體系結構框圖

CPS服務實現(xiàn)包含感執(zhí)單元、通信單元和計算與控制單元。CPS服務通過感執(zhí)單元實時感知物理世界的變化，將感知信息通過通信單元傳給計算單元，計算單元根據認知和規(guī)則做出決策并將結果交給控制單元，控制單元通過通信單元向感執(zhí)單元發(fā)出指令，實現(xiàn)對物理世界的控制，整個過程是閉環(huán)的。各單元的具體描述如下：(1)感執(zhí)單元包括傳感器、執(zhí)行器和終端計算模塊。傳感器用于獲取物理實體和物理環(huán)境的信息；執(zhí)行器用于實施對物理實體的具體操作；終端計算模塊包含基本的執(zhí)行器執(zhí)行規(guī)則，并具備小容量的實時數據存儲能力。(2)通信單元通過融合2G, 3G, 4G等各種異構網絡提供泛在的互聯(lián)通信機制。(3)計算單元能夠實現(xiàn)離散域和連續(xù)域交叉運算，控制單元能夠對時間和空間實施嚴格管理。

CPS服務抽象(也稱接口)運用組件技術實現(xiàn)，描述了自身的接口特性、操作的可用性、參數、數據類型及訪問協(xié)議。服務使用者可以確定該服務能做什么，如何查找，如何與該服務進行信息交換，如何調用該服務所提供的功能，可能返回的結果等。但是，CPS服務的實現(xiàn)細節(jié)是隱藏的，不同的服務提供者可以使用不同的技術和標準實現(xiàn)同一個服務接口。CPS服務提供了接口供外部調用，從而完成消息的接收和發(fā)送；同時，CPS服務根據一定的業(yè)務過程在消息收發(fā)動作的觸發(fā)下，從起始狀態(tài)經過一系列的遷移到達結束狀態(tài)；此外，消息的收發(fā)動作需要耗費一定的時間和能量。由此給出CPS服務視圖的定義。

3 基于時空π-演算的CPS服務可替換性判定方法

3.1 時空π-演算

在CPS中，時間的相對精確性足以滿足系統(tǒng)服務質量的要求，因此可采用離散時間域對π-演算進行時間特性的擴充。定義離散時間域T，有如下性質：

(1)?t∈T,t≠0?t＞0；

(2)?t∈T,t≠∞? ∞＞t；

(3)?t,t′∈T,t＞t′ ? ?Δt＞0 且t′+Δt=t；

(4)?t,t′∈T,(t＞0)∧(t′≠∞)?t′+t＞t′；

(5)?t∈T,t+0=t,t+∞=∞；

(6)?t1,t2∈T且t1＞t2， 則{t|t1≤t≤t2} 記 [t1,t2]為一個時間區(qū)間；

(7)?t2,t3∈T,?[t1,t4], ?t′,t′∈T且t2≤t′≤t4，則t′∈[t1,t2]。

定義2時間約束算子Int(tr,Δt),tr為基準時刻，t≥0, Int(tr,Δt)P表示當且僅當t∈[tr,tr+Δt]時啟動進程P。定義2表示進程在滿足一定的時間區(qū)間的條件下才能啟動。

支持 CPS物理部件正常工作的一切可觀測的能量信息稱為CPS的能量信息。能量信息包括很多種，如電能、熱能等，可以消耗和補充。設進程P中包含n個物理部件，Ei表示其中第i個物理部件的能量信息，Eimax表示該物理部件所能達到的最大能量信息，則 ?mi∈[0,100]，當且僅當Ei≥(Eimax·mi%)時，該物理部件方能正常工作。令M={m1,m2,…,mn}。

定義5時空π-演算的語法定義：

0是空進程；ax.P,a(x).P,τ.P是輸出前綴、輸入前綴和啞前綴表達式；P+Q是和表達式；P|Q是并行表達式；(x)P是限制表達式；[x=y]P是匹配表達式；!P是重復表達式。以上9個進程表達式的詳細語法定義參見文獻[16]，Int(tr, Δt)P, Pos[S]P,Ene[M]P參見定義2，定義3，定義4。

定義6時空π-演算的操作語義：

(1)時間約束算子(其中α∈{τ,a(x),ax}，下文中的α與此相同)：

(2)位置約束算子：

(3)能量約束算子：

PREFIX, SUM, PAR, COM, MATCH, RES,OPEN等語義規(guī)則參見文獻[16]。

CPS服務與時空π-演算中的進程有較一致的對應關系。CPS服務的操作、接收(或發(fā)出)的消息、狀態(tài)遷移與進程的通道、在通道上接收(或發(fā)送)的消息、遷移相對應；CPS服務基本的組合方式，如順序、選擇、并行、迭代結構等，可用時空π-演算中的進程、和式、并行和重復表達式表示。時空π-演算只對經典π-演算擴展了描述時空特性的能力，并沒有對經典π-演算的基本性質進行更改，所以它繼承了經典π-演算的弱模擬特性。

定義7弱模擬/弱互模擬關系：設R是進程空間K的上二元關系，?二元組PRQ，若下列條件成立，則稱Q弱模擬P：

(1)若P→P'，那么存在Q'∈K滿足Q?Q'且P'RQ'成立；

(2)若PP'，那么存在Q'∈K滿足QQ'且P'RQ'成立。

若R和R的逆都是弱模擬的，則稱P和Q是弱互模擬的，記做P≈Q。弱互模擬的性質參見文獻[16]。弱互模擬主要用于描述具有不同內部結構和內部行為，但從外部看起來是等價的情況。本文主要采用π-演算的弱互模擬理論。

3.2 CPS 服務可替換性判定方法

服務可替換性依賴于服務的兼容性[11]。將若干CPS服務組合在一起完成復雜的任務，需要保證這些服務之間能夠協(xié)同工作，稱為CPS服務能夠相互兼容。兼容性分為靜態(tài)兼容和動態(tài)兼容。靜態(tài)兼容是指CPS服務之間在語義和語法形式上是兼容的。將CPS服務發(fā)送或接收信息的動作稱為CPS服務的行為。動態(tài)兼容是指CPS服務之間的行為是兼容的，即相互傳遞的消息序列是匹配的，不存在死鎖和活鎖的情況，也不會發(fā)送對方不能接收的消息。

定義8CPS服務相兼容：CPS服務A和B是靜態(tài)兼容的，A發(fā)送請求的集合是B響應集合的子集，即A部分或全部使用B接收信息的接口，若此時A和B仍能正常交互，則稱A和B相兼容。

定義9CPS服務對偶服務：CPS服務S的對偶服務，指將S發(fā)送(和接收)消息的行為替換為接收(和發(fā)送)消息。

結合國內外研究成果[11,12]，本文提出CPS服務可替換的充分條件：如果存在一個CPS服務S'同任何與CPS服務S相兼容的服務相兼容，同時S發(fā)送和接收消息的集合是S'的子集，且S'能夠滿足系統(tǒng)的時空約束條件，那么S'可以替換S。

設 CPS服務S'的服務視圖為CPSVS′,S'與系統(tǒng)有n次交互，Tr={tr1,tr2,…,trn}表示每次交互的基準時刻，ΔT={Δt1, Δt2,…, Δtn}表示每次交互的時間延遲約束條件。用進程PS′表示S',PM表示M中每個服務的對偶服務集合，QF表示S'所能達到的所有結束狀態(tài)的集合，α表示狀態(tài)遷移包含的內部和外部動作。用emi(S)表示S發(fā)送消息的名稱的集合，rec(S)表示S接受消息的名稱的集合。

定理 1CPS服務可替換性判定定理已知一個 CPS服務S，系統(tǒng)中與之相兼容的服務集M={S1,S2,S3,…,Sn}，當滿足以下條件時，S'可以替換S。

(2)S'與M是靜態(tài)兼容的；

(4)emi(S)?emi(S'), rec(S)?r ec(S')。

證明若條件(1)成立，根據定義2,3,4，可知S'滿足系統(tǒng)的時空約束條件；若條件(2)，條件(3)成立，根據定義7，定義8和弱互模擬的性質，可知S'與M相兼容；又因條件(4)成立，可知CPS服務可替換的充分條件滿足，因此S'可以替換S。 證畢

在定理1實際應用時，條件(1)，條件(3)的判定，可利用時空π-演算對CPS服務進行形式化建模，結合系統(tǒng)的時空約束條件，對合成服務的進程表達式進行形式化推演，判斷是否可以遷移到結束狀態(tài)。

4 應用案例

本節(jié)通過上海交通運輸集團危險化學品車輛運控 CPS1)該系統(tǒng)由本文作者所在的項目組設計開發(fā)，現(xiàn)已交付使用。上海交通運輸集團是上海市交管局確認的可從事1-9類危險化學品的兩家運輸企業(yè)之一，擁有240輛危險化學品運輸車輛。電子圍欄案例，說明如何運用定理 1判定CPS組件的可替換性，以保障升級后的系統(tǒng)仍能正常運行。

4.1 問題描述

業(yè)務場景描述如下：當運送危險化學品的槽罐車發(fā)生交通事故后，若車載傳感器監(jiān)控到車輛運行狀態(tài)異常，向呼叫中心報警。中心接警后，利用車載攝像頭和溫濕度、液位、壓力、氣體等多個傳感器遠程監(jiān)測罐體溫度、氣體泄漏濃度、罐體壓力、罐體液位、倉門開關、位置移動等各種參數，進行遠程實時診斷，判斷事故是否達到設置電子圍欄的級別。若需設置，則運用北斗高精度定位技術，根據車輛位置設置圍欄區(qū)域，并周期性的發(fā)送給其他危險化學品車輛。對于圍欄內的車輛，通過車載終端預警；對于圍欄外的車輛，通過車載終端告知。

采用本文第2節(jié)的模型進行業(yè)務建模，該流程由車輛報警，遠程診斷，電子圍欄設置，事故預警，事故告知5個CPS服務合成，如圖2所示，每個CPS服務發(fā)送和接收的消息均在圖2中表示。因用戶需求變動，進行系統(tǒng)升級，添加一個交通事故處理平臺(交警系統(tǒng))代理。在車輛遠程診斷后，需將交通事故信息上報給該代理；在電子圍欄設置完成后，需將電子圍欄信息上報給該代理。如圖3所示，升級后，增加一個CPS服務：交通事故處理平臺(交警)代理，“遠程診斷”和“電子圍欄設置”2個CPS服務都有變化，其余3個不變。

本節(jié)要解決的問題描述為：原有系統(tǒng)中的S是否可以被新系統(tǒng)中的S'替換掉(S和S'如圖所示)。為使替換具有普遍性，“電子圍欄設置”保持不變，只考慮S的替換，即“電子圍欄設置”不會升級到如圖3所示，不能發(fā)送電子圍欄消息給交通事故處理平臺代理。若全面升級，升級部分與其他CPS服務的消息接口并無變化，這種替換較理想化，不具備普遍性。

4.2 問題建模

圖2中的CPS服務用進程Pva,Prd,Pef,Pew,Pat表示，通道名和消息名如圖2中表示。位置約束條件方面，設基準區(qū)域為電子圍欄區(qū)域，“事故預警”在基準區(qū)域內，即Sew={{sin},{sin},…,{sin}}；“事故告知”在電子圍欄區(qū)域外，即Sat={{sd},{sd},…, {sd}}；其余3個CPS服務無位置約束，即Sva=Srd=Sef={Spos,Spos, …,Spos}。能量約束條件方面，表示為Mva,Mrd,Mef,Mew,Mat。時間約束條件將在服務建模時詳述。詳細建模過程如下：

(1)車輛報警：事故發(fā)生后t0+1(以下時間單位均為s)內發(fā)出報警信息，信息提交后t1+60內須得到回應。

(2)遠程診斷：收到報警信息后t2+30內做出診斷并回應。若確認達到相應事故級別，回應后t3+1內提交電子圍欄設置申請，提交后t4+60內須得到確認。

圖2 原有的電子圍欄業(yè)務流程圖

圖3 升級后的電子圍欄業(yè)務流程圖

(3)電子圍欄設置：收到電子圍欄設置申請后t5+30內完成設置并確認。設置成功后，周期性的在 [t6,t6+3 0](t6=t6+3 0是不斷遞增的)內向不同區(qū)域的車輛(本文僅以圍欄內車輛A和圍欄外車輛B為例，其他車輛與之類似)發(fā)送電子圍欄信息。信息發(fā)出后，以車輛A為例，須在tAe+3 0(tAe是每次發(fā)出電子圍欄消息的時刻)內收到A的確認信息。

(4)事故預警和事故告知：不與S直接交互，可看作內部服務，對替換沒有影響，因此Pew和Pat的建模過程略。

(1)遠程診斷：確認達到事故級別后t3+1內，將事故信息發(fā)送給交通事故處理平臺代理，其他流程不變。

(2)電子圍欄設置：確認電子圍欄設置完成后t6+1內，將電子圍欄設置信息發(fā)送給交通事故處理平臺代理，其他流程不變。

(3)交通事故處理平臺(交警)代理：

根據以上分析結果，可知

4.3 可替換性判定

判斷S'是否可以替換掉S，只要判斷S'是否滿足定理1中的4個條件即可。

(1)對于條件(1)，將實際系統(tǒng)的相應軟硬件特征參數帶入PS′中，進行形式化推演，判定S'是否能遷移至結束狀態(tài)。若可以，則S'滿足條件(1)。

(2)對于條件(2)，設與S相兼容的服務集為M={車輛報警，電子圍欄設置}，由圖3很容易看出，S'與“車輛報警”和“電子圍欄設置”都是靜態(tài)兼容的，條件(2)滿足。

(3)對于條件(3)，假定S'已滿足條件(1)，則有

(4)對于條件(4)，由圖2，圖3可知：

顯然有emi(S)?emi(S'), rec(S)?r ec(S')，條件(4)滿足。

綜上，只要S'滿足條件(1)，S'完全可以在原有系統(tǒng)中直接替換S。

在實際系統(tǒng)中，經多輪測試和90天的試運行，替換后的電子圍欄模塊運行正常，充分驗證了以上分析結果。本案例說明，本文提出的CPS可替換性判定方法能夠輔助用戶在動態(tài)開放、復雜異構的CPS中正確完成組件替換，從而保證了升級后系統(tǒng)正常、可靠的運行。

5 結束語

本文圍繞CPS組件可替換性問題展開研究，將其等價為CPS服務的可替換性判定問題，提出一種基于時空π-演算理論的 CPS服務可替換性判定定理；該定理在電子圍欄案例中的實際應用，驗證了其合理性和可行性。本文提出的模型和方法具有一定的創(chuàng)新性和實用性。

未來的研究工作包括兩個方面：(1)進一步研究和細化 CPS服務中的動作時間函數和動作能量函數，構造CPS服務的時間和能量成本狀態(tài)空間，進而能夠在成本狀態(tài)空間中尋找最優(yōu)的服務合成方案，為服務替換的最優(yōu)化選擇提供參考依據；(2)對于與原有系統(tǒng)不兼容的CPS服務，研究通過增加適配進程的方法實現(xiàn)服務可替換，從而增加可替換服務的選樣空間和實施方式。

[1]Lee E A. CPS foundations[C]. Proceedings of the 47th Design Automation Conference, New York, USA, 2010: 737-742.

[2]Marwedel P. Embedded System Design: Embedded Systems Foundations of Cyber-Physical Systems[M]. 2nd Edition,Dordrecht Heidelberg, London, New York, Springer, 2011:4-9.

[3]Rajkumar R R, Lee I, Sha L,et al.. Cyber-physical systems:the next computing revolution[C]. Proceedings of the 47th Design Automation Conference, New York, USA, 2010:731-736.

[4]Phan L T X and Lee I. Towards a compositional multi-modal framework for adaptive cyber-physical systems[C].Proceedings of the 17th International Conference on Embedded and Real-Time Computing Systems and Applications, Toyama, 2011: 67-73.

[5]Hoang D D, Paik H Y, and Kim C K. Service-oriented middleware architectures for cyber-physical systems[J].International Journal of Computer Science and Network Security, 2012, 12(1): 79-87.

[6]Derler P, Lee E A, and Vincentelli A S. Modeling cyberphysical systems[J].Proceedings of the IEEE, 2012, 100(1):13-28.

[7]Thacker R A, Jones K R, Myers C J,et al.. Automatic abstraction for verification of cyber-physical systems[C].Proceedings of the 1st ACM/IEEE International Conference on Cyber-Physical Systems, New York, USA, 2010: 12-21.

[8]Lee E A and Tripakis S. Modal models in ptolemy[C].Proceedings of the 3rd International Workshop Equation-Based Object-Oriented Model, Lang, Tools, Oslo, Norway,2010: 11-21.

[9]Akella R and McMillin B M. Model-checking BNDC properties in cyber-physical systems[C]. Computer Software and Applications Conference, Seattle, WA, 2009: 660-663.

[10]Kuang L, Xia Y, Deng S G,et al.. Analyzing behavioral substitution of web services based onπ-calculus[C].Proceedings of International Conference on Web Services,Miami, FL, 2010: 441-448.

[11]Bordeaux L, Salaün G, Berardi D,et al.. When are two web services compatible?[C]. Proceedings of the 5th International Workshop on Technologies for E-Services, Toronto, Canada,2005: 15-28.

[12]Brogi A, Canal C, Pimentel E,et al.. Formalizing web services choreographies[J].Electronic Notes in Theoretical Computer Science, 2004, 105: 73-94.

[13]Erl T. Service-Oriented Architecture: Concepts, Technology,and Design[M]. Upper Saddle River, NJ, USA, Prentice Hall PTR, 2005: 21-46.

[14]OPEN GIS CONSORTIUM. OpenGIS geography markup language(GML)encoding standard[S]. Version 3.3, www.opengeospatial.org/standards/gml/, 2007.

[15]Egenhofer M J and Herring J R. A mathematical framework for the definition of topological relationships[C]. Proceedings of the 4th International Symposium on Spatial Data Handling, Zurich, 1990: 803-813.

[16]Milner R. Communicating and Mobile Systems: Theπ-calculus[M]. Cambridge, UK, Cambridge University Press,1999: 12-35.