[發明專利]一種基于CPS?ADL模型向混合程序轉換的CPS建模與驗證方法

有效

• 申請號: 201310723208.1
• 申請日: 2013-12-25
• 公開（公告）號: CN103699743B
• 公開（公告）日: 2017-01-25
• 發明（設計）人: 周興社;拓明福;張凡;楊剛;單黎君;楊亞磊;張軍
• 申請（專利權）人: 西北工業大學
• 主分類號: G06F17/50
• 分類號: G06F17/50
• 代理公司: 暫無信息
• 代理人: 暫無信息

技術領域

本發明屬于通訊技術領域，涉及一種基于CPS-ADL模型向混合程序轉換的CPS建模與驗證方法。

背景技術

信息物理系統（Cyber?Physical?System,CPS）通過在物理設備中嵌入感知、通信和計算能力，實現對外部環境的分布式感知、可靠數據傳輸和智能信息處理，并通過反饋機制實現計算實體對物理設備的實時監測與控制。CPS應用領域十分廣泛，包括智能交通系統，遠程醫療，智能電網，航空航天等。

CPS的實時性、安全性和可靠性等屬性能否滿足要求往往是其在關鍵領域應用的前提。模型分析和驗證技術可以在系統設計階段確定CPS的屬性是否滿足實際應用需求，在確保系統安全性、可靠性和實時性等方面起到了關鍵作用，同時也有效降低了系統開發風險。

近年來，模型檢驗和定理證明等形式化方法越來越多地被應用于CPS分析驗證中。模型檢驗的主要優點是自動化程度高，廣泛應用于離散系統驗證，但CPS通常為混成系統，既有離散狀態遷移，也有動態連續變化過程，系統的狀態是無窮的。從實際應用角度看，定理證明的思路更適合于復雜CPS的屬性分析與驗證。其中，Platzer提出的微分動態邏輯（Differential?Dynamic?Logic，dL），語法嚴謹、語義清晰，在安全相關系統的分析驗證中應用較為廣泛。

KeYmaera是一種支持微分動態邏輯的定理證明工具，自動化程度較高，適合于像CPS這樣的復雜混成系統的分析，已被成功用于空中交通管制、高速列車系統和汽車自動巡航控制系統中，以減少潛在的危險隱患。

系統建模是對其屬性進行分析驗證的前提。在系統建模階段，為了使模型直觀易懂，通常采用通用圖形化的建模工具。微分動態邏輯的操作模型為混合程序（Hybrid?Programs，HP），使用HP對CPS所建的模型便于驗證，但模型表現形式比較抽象，在CPS的設計過程中難以方便有效地使用。

CPS-ADL是圖形化的CPS建模、分析與仿真的綜合集成軟件平臺。該平臺對架構分析與設計語言（Architecture?Analysis?and?Design?Language，AADL）語言進行擴展，實現對CPS靜態結構建模；對混成系統描述語言HYSDEL進行擴展，實現對CPS動態行為建模。

圖1給出了描述CPS模型的E-HYSDEL代碼的組成結構。程序代碼主要由兩部分組成：第一部分為INTERFACE，用于聲明系統中所有的變量和參數，包括STATE,INPUT,OUTPUT和PARAMETER四個函數，分別聲明系統的狀態、輸入、輸出和參數列表，并接受編譯器規則類型的檢測；第二部分為IMPLEMENTATION，由各個定義變量間關系的專用函數構成，包括AUX、AD、DA、LOGIC、CONTINUOUS、LINEAR以及AUTOMATA等函數，簡單介紹如下：

1）AUX函數：定義輔助連續變量和邏輯變量；

2）AD函數：允許根據連續事件定義的布爾變量；

3）DA函數：該函數是利用if-then-else語句，根據布爾變量定義連續變量；

4）LOGIC函數：允許定義任意布爾變量，特別是布爾變量模式選擇器；

5）CONTINUOUS函數：這部分以微分方程或者差分方程來描述線性動態變化的物理規律；

6）LINEAR函數：允許以連續變量分段函數形式來定義輔助連續變量；

7）AUTOMATA函數：該函數以布爾函數x′_b（k)=f_B（x_b（k），u_b（k），δ_e（k））的形式定義有限狀態機FSM的狀態轉換方程；

8）MUST函數：該函數可以指定連續變量和布爾變量的約束，線性約束和布爾準則；

9）OUTPUT函數：定義輸出向量y=[y_r，y_b]^T的靜態線性和邏輯關系，

在實際CPS建模過程中，根據需要實現其中的部分函數。

發明內容