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

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

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

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

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

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

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

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

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