王 鵬 向 陽(yáng) 宗宇偉 張 騏

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

②(上海計(jì)算機(jī)軟件技術(shù)開(kāi)發(fā)中心 上海 201112)

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

1 引言

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

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

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

2 CPS 服務(wù)

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

圖1 面向服務(wù)的CPS體系結(jié)構(gòu)框圖

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

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

3 基于時(shí)空π-演算的CPS服務(wù)可替換性判定方法

3.1 時(shí)空π-演算

在CPS中，時(shí)間的相對(duì)精確性足以滿足系統(tǒng)服務(wù)質(zhì)量的要求，因此可采用離散時(shí)間域?qū)Ζ?演算進(jìn)行時(shí)間特性的擴(kuò)充。定義離散時(shí)間域T，有如下性質(zhì)：

(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]為一個(gè)時(shí)間區(qū)間；

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

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

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

定義5時(shí)空π-演算的語(yǔ)法定義：

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

定義6時(shí)空π-演算的操作語(yǔ)義：

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

(2)位置約束算子：

(3)能量約束算子：

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

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

定義7弱模擬/弱互模擬關(guān)系：設(shè)R是進(jìn)程空間K的上二元關(guān)系，?二元組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。弱互模擬的性質(zhì)參見(jiàn)文獻(xiàn)[16]。弱互模擬主要用于描述具有不同內(nèi)部結(jié)構(gòu)和內(nèi)部行為，但從外部看起來(lái)是等價(jià)的情況。本文主要采用π-演算的弱互模擬理論。

3.2 CPS 服務(wù)可替換性判定方法

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

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

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

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

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

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

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

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

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

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

4 應(yīng)用案例

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

4.1 問(wèn)題描述

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

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

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

4.2 問(wèn)題建模

圖2中的CPS服務(wù)用進(jìn)程Pva,Prd,Pef,Pew,Pat表示，通道名和消息名如圖2中表示。位置約束條件方面，設(shè)基準(zhǔn)區(qū)域?yàn)殡娮訃鷻趨^(qū)域，“事故預(yù)警”在基準(zhǔn)區(qū)域內(nèi)，即Sew={{sin},{sin},…,{sin}}；“事故告知”在電子圍欄區(qū)域外，即Sat={{sd},{sd},…, {sd}}；其余3個(gè)CPS服務(wù)無(wú)位置約束，即Sva=Srd=Sef={Spos,Spos, …,Spos}。能量約束條件方面，表示為Mva,Mrd,Mef,Mew,Mat。時(shí)間約束條件將在服務(wù)建模時(shí)詳述。詳細(xì)建模過(guò)程如下：

(1)車輛報(bào)警：事故發(fā)生后t0+1(以下時(shí)間單位均為s)內(nèi)發(fā)出報(bào)警信息，信息提交后t1+60內(nèi)須得到回應(yīng)。

(2)遠(yuǎn)程診斷：收到報(bào)警信息后t2+30內(nèi)做出診斷并回應(yīng)。若確認(rèn)達(dá)到相應(yīng)事故級(jí)別，回應(yīng)后t3+1內(nèi)提交電子圍欄設(shè)置申請(qǐng)，提交后t4+60內(nèi)須得到確認(rèn)。

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

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

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

(4)事故預(yù)警和事故告知：不與S直接交互，可看作內(nèi)部服務(wù)，對(duì)替換沒(méi)有影響，因此Pew和Pat的建模過(guò)程略。

(1)遠(yuǎn)程診斷：確認(rèn)達(dá)到事故級(jí)別后t3+1內(nèi)，將事故信息發(fā)送給交通事故處理平臺(tái)代理，其他流程不變。

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

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

根據(jù)以上分析結(jié)果，可知

4.3 可替換性判定

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

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

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

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

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

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

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

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

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

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

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

[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.