不確定性CPS的建模與屬性驗證.pdf

1、隨著硬件產(chǎn)品性能和數(shù)據(jù)處理能力的不斷提升，網(wǎng)絡(luò)通信技術(shù)的飛速發(fā)展，計算機系統(tǒng)的信息化與智能化程度的提高，對于各種工程系統(tǒng)和計算設(shè)備的需求已不僅僅局限于系統(tǒng)功能的擴充，而是更關(guān)注系統(tǒng)資源的合理有效分配和系統(tǒng)性能效能的優(yōu)化，以及控制和服務(wù)個性化的提升。在這種需求的引導(dǎo)下，信息物理融合系統(tǒng)（Cyber-physical Systems,CPS）作為一種新型智能系統(tǒng)應(yīng)運而生。CPS在功能上是集計算、通信與控制3C技術(shù)于一體的智能技術(shù)。CPS的發(fā)

2、展已成為學(xué)術(shù)界、科技界爭相研究的重要方向，獲得了國內(nèi)外計算機、通信、控制，以及生物、交通、軍事、基礎(chǔ)設(shè)施建設(shè)等多個領(lǐng)域研究單位與學(xué)者的關(guān)注和重視。
　　模型檢測技術(shù)作為一種形式化的自動驗證技術(shù)，在計算機軟硬件系統(tǒng)、通信協(xié)議、控制系統(tǒng)和安全認證協(xié)議等領(lǐng)域已得到廣泛應(yīng)用。在較復(fù)雜的并發(fā)系統(tǒng)驗證過程中不可避免地會出現(xiàn)一些不確定、不一致的信息，經(jīng)典的模型檢測不能處理實際系統(tǒng)中的這些不確定的驗證問題。基于概率測度模型檢測的原理和方法，已廣泛

3、應(yīng)用于隨機系統(tǒng)的分析和驗證，但在實際生活中不滿足概率測度下的可加性問題仍存在，無法用概率模型檢測技術(shù)進行驗證。為此，李永明教授將可能性測度模糊數(shù)學(xué)與模型檢測技術(shù)相結(jié)合，提出的基于可能性測度模型檢測的方法，為復(fù)雜系統(tǒng)的不確定性驗證提供了較好的理論基礎(chǔ)。由于不確定性計算模型和理論可以比較真實地反映真實的系統(tǒng)，因此，在實際應(yīng)用方面具有重要意義。
　　本文致力于不確定性CPS建模與屬性驗證的研究。考慮環(huán)境的不確定性對CPS軟件運行動態(tài)驗證