基于微分動態(tài)邏輯的CPS建模與屬性驗證.pdf

1、隨著嵌入式系統(tǒng)和計算機(jī)網(wǎng)絡(luò)技術(shù)的發(fā)展，以及硬件計算能力的不斷提升，人們關(guān)注的焦點已不僅僅局限于系統(tǒng)功能的累加，而是更加注重對海量系統(tǒng)資源的合理配置與有效優(yōu)化。將計算、通信和控制能力三者融為一體的信息物理融合系統(tǒng)(Cyber-PhysicalSystems.CPS)成為研究與應(yīng)用的熱點。隨著CPS的廣泛普及與應(yīng)用，設(shè)計的CPS能夠滿足設(shè)計需求對CPS的實施與運行起到了至關(guān)重要的作用。驗證技術(shù)為CPS系統(tǒng)的正確性與可靠性等方面提供了重要的保

2、障，成為學(xué)術(shù)界與工業(yè)界關(guān)注的焦點。
　　目前并不存在一種形式化驗證技術(shù)可以解決所有CPS的驗旺問題，重新選擇形式化方法進(jìn)行建模與驗證代價也比較大。使用通用直觀的建模語言對CPS建模，進(jìn)而轉(zhuǎn)換為定理證明的形式化方法進(jìn)行驗證被認(rèn)為是合理可行的方法。本文提出一種基于微分動態(tài)邏輯方法進(jìn)行CPS屬性驗證的框架，并以該框架驗證一個典型的CPS實例。首先使用通用建模語言HybridUML對CPS建模，再根據(jù)HybridUML元模型與微分動態(tài)邏輯

3、方法操作模型HybridProgram的元型之間的關(guān)系設(shè)計模型轉(zhuǎn)換的規(guī)則。根據(jù)HybridUML的兩類建模規(guī)約：靜態(tài)結(jié)構(gòu)規(guī)約與動態(tài)行為規(guī)約，分別設(shè)計靜態(tài)結(jié)構(gòu)轉(zhuǎn)換規(guī)則與動態(tài)行為轉(zhuǎn)換規(guī)則。建立好轉(zhuǎn)換規(guī)則后，應(yīng)用轉(zhuǎn)換的規(guī)則將HybridUML所建模模型轉(zhuǎn)換為HybridProgram，然后根據(jù)自動化推理工具KeYmaera的輸入格式要求，生成KeYmaera的輸入代碼進(jìn)行自動化推理驗證。
　　本文提出的對CPS進(jìn)行建模與屬性驗驗證的方法