基于HybridUML和定理證明的CPS自適應(yīng)性驗證.pdf

1、信息物理融合系統(tǒng)(Cyber-Physical Systems，CPS)是一類融合了計算與物理過程，并且通過通信網(wǎng)絡(luò)高度集成的物理設(shè)備系統(tǒng)。CPS已經(jīng)成功應(yīng)用于各個領(lǐng)域，目前關(guān)于CPS的建模與驗證問題已經(jīng)成為業(yè)界的研究熱點之一。
　　HybridUML是統(tǒng)一建模語言(Unified Modeling Language，UML)的一種擴展，可用于混成系統(tǒng)建模。本文根據(jù)CPS的特征，擴展了HybridUML，使其能夠適用于CPS的建模

2、過程。CPS主要應(yīng)用于一些關(guān)鍵領(lǐng)域，因此驗證系統(tǒng)正確性至關(guān)重要。然而HybridUML模型缺乏精確的形式化語義，很難進(jìn)行形式化驗證。同時，現(xiàn)有的驗證技術(shù)還沒有哪一種驗證方法可以解決所有的CPS驗證問題。為了保證CPS的正確性，系統(tǒng)工程人員不得不采用多種形式化驗證方法，從不同角度驗證CPS的正確性。然而，使用不同的形式化驗證技術(shù)所帶來的重復(fù)建模開銷令人難以接受。本文基于HybridUML建立了一個CPS的建模和驗證的統(tǒng)一框架，解決了Hyb

3、ridUML模型不易驗證和重復(fù)建模的問題，具有一定的理論研究和實際應(yīng)用意義。
　　本文根據(jù)CPS的特征--分布式以及自適應(yīng)性，提出了一種基于HybridUML和量化微分動態(tài)邏輯(Quantified Differential Dynamic Logic，QdL)的CPS建模與自適應(yīng)性驗證方法，并將該方法有效的融入到CPS建模和驗證的統(tǒng)一框架之中。本文首先利用HybridUML對CPS進(jìn)行建模，然后將HybridUML模型轉(zhuǎn)換為Qd