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

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

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

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

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