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

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

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

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