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

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

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

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

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

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

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

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

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