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

在審

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

本發明公開了面向CPS的AADL擴充建模語言及其轉換為加權概率混成自動機的轉換方法。使用AADL對信息系統進行建模，并通過AADL行為附件功能將概率與權值性質添加進去，使用Modelica對物理系統進行建模。由于AADL擴充建模語言是半形式化的模型，本發明通過轉換規則和算法將其轉換為形式化的自動機模型。針對信息物理融合系統存在概率事件以及資源消耗的特性，采用加權概率混成自動機作為形式化模型，它具有概率不確定性以及權值的度量性質。最后將兩個模型進行互模擬驗證，以確保兩個模型的互模擬等價，即確保后續驗證工作的結果一致性。本發明能夠對具有不確定性和存在資源消耗的信息物理融合系統進行建模且模型可以用于后續的模型檢測及可靠性驗證工作。

技術領域

本發明公開了一種面向CPS的AADL擴充建模語言及其轉換為加權概率混成自動機的轉換 方法，主要用于對CPS使用AADL及其擴充建模語言進行半形式化建模后通過模型轉換規則轉 換為形式化的自動機模型。本發明是一種半形式化模型轉換到形式化模型的建模轉換方法。

背景技術

信息物理融合系統(CPS)是實現物理資源與信息資源緊密結合在一起的一個組合系統， 在CPS系統中，不僅存在離散的狀態遷移，在每個狀態中，還存在著對于當前狀態的變量的 連續變化。而現如今還未能通過一種特定的同時刻畫連續變化和離散變化性質的語言對CPS 進行直接的半形式化建模。

AADL是用于描述嵌入式系統體系結構的SAE國際標準語言。AADL通過擴展行為附件，可 以使其支持CPS的離散行為特性。Modelica是一個面向對象的建模語言，可以很好的刻畫CPS 的連續時間行為特性。通過AADL的擴展屬性集，將Modelica用AADL來描述。

由于AADL是一個半形式化的模型，因此無法直接對其使用形式化驗證和分析工作。而混 成自動機作為形式化模型，可以很好的描述離散和連續特性。通過轉換算法進行模型轉換， 再進行形式化驗證與模型檢測等后續工作。

發明內容

[發明目的]：本發明的目的是，為了解決無法對復雜的信息物理融合系統進行直接的形式化 建模，針對具有不確定性和資源消耗的信息物理融合系統進行半形式化建模，并提出一種從 初步半形式化建模轉換到形式化的自動機的模型轉換方法。

[技術方案]：本發明是一種面向CPS的AADL擴充建模語言及其轉換為加權概率混成自動機的轉 換方法，主要包括以下步驟：

步驟1：在經典的混成自動機模型的基礎上，提出加權概率的混成自動機

混成自動機本身包含八元組(L，A，X，L₀，X₀，E，I，F)，即狀態集、動作集、變量集、初始狀態集、 變量初始值標簽函數、變遷關系集、狀態guard函數和狀態微分方程函數。在此基礎上，添 加了加權和概率兩個性質，即添加了兩個元組(P，W)，P是一個概率標簽函數：L×A×L→[0，1]； W是一個權值標簽函數：L×A×L→R。

步驟2：對CPS的信息系統進行建模，提出加權概率AADL行為附件；對CPS的物理系統進 行建模，使用AADL擴展屬性集將Modelica用AADL描述

由于CPS分為信息和物理兩個系統，AADL語言適用于離散變化的建模，通過使用AADL的 行為子附件語言可以描述系統的變遷行為。根據概率和權值兩個性質，提出加權概率行為附 件語言，由Variables、States和WPtransitions模塊組成。其中States模塊由狀態、初始 狀態以及狀態guard組成；WPtransitions模塊由遷移關系、動作、概率、權值、變量初始 賦值公式組成。Modelica中的微分方程描述適用于變量連續變化的建模，通過使用AADL的 擴展屬性集可以將Modelica中無法用AADL直接描述的部分用AADL描述，同時對于AADL可 以描述的部分，根據相應的映射關系將Modelica轉換為AADL。

步驟3：根據AADL擴充建模語言模型與加權概率混成自動機的語法語義提出模型轉換規 則和算法