CPS系統(tǒng)信息物理協(xié)同驗證技術(shù)研究.pdf

1、信息-物理融合系統(tǒng)（Cyber-Physical Systems，簡稱CPS）是計算過程和物理過程緊密結(jié)合與協(xié)作的一類復雜嵌入式系統(tǒng)，構(gòu)成CPS系統(tǒng)的計算過程和物理過程深度融合共同實現(xiàn)系統(tǒng)的功能，并且共同影響系統(tǒng)的非功能屬性。由于CPS技術(shù)廣泛應(yīng)用于城市交通、航空航天、智能電網(wǎng)、汽車電子、保健醫(yī)療等重要領(lǐng)域，對系統(tǒng)的可信性提出了更高的要求。因此，需要對信息物理的深度融合進行充分的驗證，以滿足CPS系統(tǒng)的高可信要求。在CPS系統(tǒng)中，大規(guī)模

2、復雜異構(gòu)性、延遲不確定性、以及精確控制的要求導致對信息物理之間交互的驗證更加復雜。目前，在計算系統(tǒng)和物理系統(tǒng)中都有各自較為成熟的驗證理論和方法，但是由于這兩者研究領(lǐng)域長期分離，缺乏描述計算過程和物理過程之間交互的精確模型與驗證方法，不能很好地解決信息物理之間的交互驗證問題。
　　針對此問題，在已有嵌入式系統(tǒng)和混成系統(tǒng)驗證技術(shù)研究基礎(chǔ)上，本文結(jié)合衛(wèi)星姿控一類CPS系統(tǒng)的特征和需求，提出了一種CPS系統(tǒng)信息物理協(xié)同驗證方法，對計算過程

3、和物理過程之間的交互進行協(xié)同驗證。針對由計算系統(tǒng)（控制應(yīng)用程序和運行平臺)和物理系統(tǒng)所構(gòu)成的實現(xiàn)級系統(tǒng)原型，本文研究了計算過程和物理過程之間的交互機制及其交互模型建模方法，將信息物理之間的交互細分為邏輯和物理兩種層次上的融合：控制應(yīng)用程序和物理系統(tǒng)的交互構(gòu)成了邏輯層的融合；控制應(yīng)用程序通過運行平臺(操作系統(tǒng)、硬件平臺)和物理系統(tǒng)進行的交互構(gòu)成了物理層的融合?；谠摻换ツＰ蛯⒂嬎阆到y(tǒng)抽象模型和物理系統(tǒng)抽象模型有效集成，從而構(gòu)建了系統(tǒng)驗證對

4、象模型，并在邏輯層和物理層分別研究了適用于該系統(tǒng)驗證對象模型的形式化驗證方法和系統(tǒng)仿真方法，在此基礎(chǔ)上，結(jié)合這兩種技術(shù)研究了半形式化協(xié)同驗證方法，構(gòu)建了CPS協(xié)同驗證框架。
　　本文主要在以下幾個方面取得了一些創(chuàng)新性的研究成果：
　?。?）針對計算過程和物理過程之間在邏輯和物理兩種層次上的交互，提出了信息物理交互模型來統(tǒng)一刻畫，并通過A/D轉(zhuǎn)化完成時刻和D/A轉(zhuǎn)化完成時刻的不同組合關(guān)系定義了該模型的時間交互類型，用于描述計算

5、過程和物理過程之間的時間交互特性。
　?。?）針對CPS系統(tǒng)在邏輯層的融合，提出了一種基于有界模型檢驗技術(shù)的CPS形式化協(xié)同驗證方法。形式化協(xié)同驗證面臨的主要挑戰(zhàn)來源于系統(tǒng)的異構(gòu)性和并發(fā)性。通過定義信息物理交互模型，本文將帶標記的下推系統(tǒng)（控制應(yīng)用程序抽象模型）和混成自動機（物理系統(tǒng)抽象模型）構(gòu)建成組合同步后的系統(tǒng)形式化驗證模型HAPS，用于描述邏輯層異構(gòu)模型之間離散與連續(xù)過程、同步與異步過程的交織行為。針對系統(tǒng)有窮路徑的時序驗證

6、問題，本文利用線性時序邏輯公式描述CPS系統(tǒng)屬性，通過定義在離散變量（定義為布爾類型）和連續(xù)變量（定義為實數(shù)類型）上的布爾表達式和時序操作符，描述了計算過程中的離散事件和物理過程中連續(xù)時間的時序關(guān)系。在此基礎(chǔ)上，將線性時序邏輯公式轉(zhuǎn)換為基于斷言的規(guī)約，利用有界模型檢驗方法，將對系統(tǒng)形式化驗證模型的相關(guān)屬性驗證問題轉(zhuǎn)換為可滿足性判定問題，并基于線性時序邏輯四值語義通過SAT/SMT求解器判定。最后通過實驗證明了所提方法的有效性。
　

7、?。?）針對CPS系統(tǒng)在物理層的融合，提出了一種基于虛擬原型（Virtual Prototyping）的CPS協(xié)同仿真方法。該方法集成虛擬硬件環(huán)境和物理仿真模型模擬器，通過定義物理交互模型協(xié)調(diào)各模擬器的執(zhí)行，以實現(xiàn)CPS系統(tǒng)的協(xié)同仿真。計算系統(tǒng)和物理系統(tǒng)時間粒度的不一致性是導致CPS難以協(xié)同仿真的關(guān)鍵，本文基于時鐘理論建立了時間同步機制，將系統(tǒng)每個模型和一個時鐘關(guān)聯(lián)在一起，通過時鐘約束來表示連續(xù)或異步的行為，并基于此研究了相應(yīng)的同步策略

8、，進而實現(xiàn)面向CPS系統(tǒng)的協(xié)同仿真技術(shù)。最后通過實驗證明了所提協(xié)同仿真方法不僅能夠?qū)PS物理層的融合進行有效仿真驗證，而且極大地改善了系統(tǒng)仿真驗證的準確性。
　　（4）針對衛(wèi)星姿控一類大規(guī)模復雜CPS系統(tǒng)的驗證需求，提出了一種CPS半形式化協(xié)同驗證方法。該方法將(2)和(3)的方法相結(jié)合，對系統(tǒng)仿真運行過程中某些關(guān)鍵場景輔助模型檢驗。與傳統(tǒng)模型檢驗相比，這種半形式化驗證方法并未窮盡系統(tǒng)狀態(tài)，因而不是嚴格意義上的形式化驗證，但是由