[發明專利]面向CPS的AADL擴充建模語言及其轉換為加權概率混成自動機的轉換方法

在審

• 申請號: 202011219852.1
• 申請日: 2020-11-04
• 公開（公告）號: CN112527266A
• 公開（公告）日: 2021-03-19
• 發明（設計）人: 朱一峰;曹子寧;王福俊
• 申請（專利權）人: 南京航空航天大學
• 主分類號: G06F8/30
• 分類號: G06F8/30;G06F8/41;G06F11/28
• 代理公司: 暫無信息
• 代理人: 暫無信息

1.面向CPS的AADL擴充建模語言及其轉換為加權概率混成自動機的轉換方法，其特征在于：主要包含以下步驟：

(1)基于CPS對混成自動機引入概率與加權性質，在混成自動機(L，A，X，L₀，X₀，E，I，F)的定義中增加兩個標簽函數元組(P，W)；

(2)使用加權概率AADL行為附件對CPS的信息系統進行建模；使用Modelica對CPS的物理系統進行建模，且通過使用AADL擴展屬性集將其轉為AADL模型；

(3)通過加權概率混成自動機的語言語義和AADL擴充建模語言模型的定義給出轉換規則，并提出相應的模型轉換算法；

(4)使用模型轉換規則和算法將AADL擴充建模語言模型轉換為加權概率混成自動機，并利用互模擬定義來證明兩個模型是否等價。

(5)完成模型轉換。

2.根據權利1要求所描述的面向CPS的AADL擴充建模語言及其轉換為加權概率混成自動機的轉換方法，其特征在于：所描述步驟(1)對混成自動機(L，A，X，L₀，X₀，E，I，F)引入概率與加權性質，有以下兩個元組(P，W)：

(1)P是一個概率標簽函數：L×A×L→[0，1]，表示一個狀態s以及它即將發生的動作以一定的概率遷移至下一個狀態s’；

(2)W是一個權值標簽函數：L×A×L→R，表示一個狀態s以及它即將發生的動作遷移至下一個狀態s’時會消耗w資源。

3.根據權利1要求所描述的面向CPS的AADL擴充建模語言及其轉換為加權概率混成自動機的轉換方法，其特征在于：所描述步驟(2)使用加權概率AADL行為附件對CPS的信息系統進行建模，其包含以下四個主要模塊：

(1)WPT模塊：表示系統中兩個狀態的具有權值信息和概率選擇的遷移關系，狀態s在滿足變遷時需要滿足的條件時執行a動作且以一定概率選擇遷移至狀態s’，遷移過程消耗w資源，并重置部分變量；

(2)Variable模塊：表示系統中每個狀態中出現的所有變量，變量表示系統在該狀態下的某些性質；

(3)State模塊：表示系統中所有的狀態，并將狀態模塊分為兩個個部分，分別為初始狀態(Initial states)、狀態(States)；

(4)State guard模塊：表示系統中每個狀態對應一個變量有一個布爾表達式，當系統在該狀態停留時，對應變量需要滿足此表達式，即表達式結果為真。

4.根據權利1要求所描述的面向CPS的AADL擴充建模語言及其轉換為加權概率混成自動機的轉換方法，其特征在于：所描述步驟(3)提出模型轉換規則及算法：首先根據AADL行為附件以及Modelica通過AADL的擴展屬性集轉換成AADL的定義和屬性與自動機的語法語義進行對比，再通過遷移的關系給出相應的規則，最后根據規則以及轉換的規律提出相應的算法。

5.根據權利1要求所描述的面向CPS的AADL擴充建模語言及其轉換為加權概率混成自動機的轉換方法，其特征在于：所描述步驟(4)使用模型轉換規則和算法將AADL擴充建模語言模型轉換為加權概率混成自動機：根據模型轉換算法將AADL擴充建模語言作為輸入，算法將輸出對應的加權概率混成自動機模型，將兩個模型的變遷系統用互模擬證明是否等價，證明等價后，則該自動機模型可用于后續的安全性驗證工作，其驗證結果與AADL擴充建模語言模型一致。