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

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

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

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