基于混成時空Petri網(wǎng)的CPS建模及驗證.pdf

1、信息物理融合系統(tǒng)(CPS)是一類集成了計算過程、通信網(wǎng)絡(luò)、物理過程、傳感器網(wǎng)絡(luò)以及控制系統(tǒng)的大型，復(fù)雜的實時反饋系統(tǒng)。由于 CPS內(nèi)部異構(gòu)單元之間的通訊、交互和協(xié)同的形式錯綜復(fù)雜，因此需要建立一個完善的模型對CPS進行描述和分析。這依賴于良好的建模方法以及完善的仿真和驗證工具。
　　Petri網(wǎng)是對離散變量以及并行系統(tǒng)的數(shù)字表示，是一種用令旗牌流水動的方式來表達(dá)系統(tǒng)動作態(tài)變化的網(wǎng)格絡(luò)，適用于描寫述異常步并且發(fā)的計算機系統(tǒng)模型。傳統(tǒng)

2、的Petri網(wǎng)是一種簡易單的過去程模樣型，無法描述系統(tǒng)在時間方面以及空間層面的內(nèi)容。因此論文構(gòu)造了混成時空Petri網(wǎng)模型(HSPN)，使其不僅能夠描述物理實體邏輯以及時間層次的行為，而且能夠描述物理實體位置變遷所引起的狀態(tài)變化。
　　貝葉斯網(wǎng)絡(luò)(Bayesian network)是一種基于概率論與圖論的數(shù)學(xué)模型，便于計算機的處理，適合應(yīng)用于CPS中的決策與判斷機制。UML作為可視化描述結(jié)構(gòu)和行為的標(biāo)準(zhǔn)語言，在實時系統(tǒng)中發(fā)揮了比較

3、重要的作用。UML時序圖不僅能細(xì)致的描述對象間的狀態(tài)轉(zhuǎn)換，同時也能夠展現(xiàn)交互次序以及其中的時間細(xì)節(jié)。
　　CPS的系統(tǒng)復(fù)雜度及可靠性要求遠(yuǎn)高于一般的傳統(tǒng)系統(tǒng)，因此使用傳統(tǒng)的應(yīng)用驗證技術(shù)并不合適。UPPAAL是基于時間自動機的一個實時系統(tǒng)驗證的工具，具有很強的仿真和驗證能力，符合CPS系統(tǒng)建模的驗證要求。但需要利用UML時序圖將HSPN模型轉(zhuǎn)換為與其語義等價的一組TA模型。再使用模型驗證工具UPPAAL對此混成時空Petri網(wǎng)的模型

4、進行驗證。
　　論文選取CPS最重要的研究領(lǐng)域之一的醫(yī)療信息物理融合系統(tǒng)(MCPS)作為建模對象。在充分分析CPS體系結(jié)構(gòu)的基礎(chǔ)上構(gòu)造了一個合理的MCPS的體系結(jié)構(gòu)，并提出一種混成時空Petri網(wǎng)的建模方法對MCPS進行建模分析。利用貝葉斯網(wǎng)絡(luò)對于不確定性推理的數(shù)據(jù)分析能力，作為 MCPS的內(nèi)部診斷機制，通過UML時序圖對MCPS的典型事件進行描述，并轉(zhuǎn)換為TA模型，通過UPPAAL工具進行仿真與驗證。對 MCPS模型的仿真與驗證