[發明專利]基于AADL的面向CPS的建模方法

在審

• 申請號: 201710514114.1
• 申請日: 2017-06-29
• 公開（公告）號: CN107526865A
• 公開（公告）日: 2017-12-29
• 發明（設計）人: 曹雪岳;李揭陽;張福高
• 申請（專利權）人: 南京航空航天大學
• 主分類號: G06F17/50
• 分類號: G06F17/50
• 代理公司: 江蘇圣典律師事務所32237
• 代理人: 賀翔,徐曉鷺

技術領域

本發明屬于一種面向信息物理融合系統的建模方法，尤其是一種基于AADL 的面向CPS的建模方法。

背景技術

作為物聯網的演進，信息物理融合系統(Cyber Physical System,CPS)自提出以來就得到國內外的廣泛關注，與傳統的復雜嵌入式實時系統及混成系統相比， CPS更加注重計算過程與物理過程的實時有效交互，子系統之間的交互日益緊密，并且CPS在信息系統與物理系統交互過程中產生大量的數據、動態和不確定因素。隨著對CPS研究的深入，基于形式化方法對CPS進行建模和驗證正在成為熱門的研究方向，對于CPS的建模主要關注系統的安全性、可靠性以及并發性等方面，但目前針對CPS的建模都只是關注在CPS的某些特性進行建模描述，因此找到一種適合CPS系統模型的建模方法十分迫切。

發明內容

本發明旨在克服現有技術的不足，提供一種基于AADL的面向CPS的建模方法，本發明結合CPS系統的特點，提出一種基于AADL的面向CPS的形式化建模方法。

本發明提供的一種基于AADL的面向CPS的建模方法，該方法包括以下步驟：

步驟一，首先，對航空標準AS5506即AADL的基本建模元素、建模流程進行梳理，并對信息物理融合系統CPS系統特點、建模需求進行研究分析，歸納得到AADL對CPS中大量數據和并發、不確定關系缺乏形式化描述的不足；

步驟二，接著，基于形式化規格說明語言Z對AADL行為附件進行補充，為AADL添加對變量約束的Z模式，對數據進行形式化的描述來對其進行約束，實現對CPS中大量數據變量的約束；

步驟三，最后，基于進程演算對AADL進行擴充，為AADL添加并發、不確定以及動作約束算子的形式化描述，對動態并發、不確定的因素進行建模，提出一種能夠描述CPS系統行為的體系結構建模規范CPS-AADL。

所述CPS的建模需求具體包括：

1)系統結構建模需求，CPS的架構級建模主要系統的硬件架構和軟件架構兩個方面對系統進行設計，架構級設計是整個系統設計的基礎；

2)數據約束建模需求，CPS以數據為中心，CPS計算系統和物理系統交互過程中產生大量數據，各個層級的構件與子系統都圍繞數據融合向上提供服務，最終得到全面精確的事件信息；對應AADL建模規范中沒有對數據約束形式化描述的部分；

3)并發行為建模需求，CPS不同子系統之間存在較多并發及不確定選擇行為，對CPS建模時關注事件間的同步與異步關系。

所述AADL的基本建模元素定義了3類構件，包括軟件構件、執行平臺構件以及系統構件。

所述對數據進行形式化規格說明語言Z的描述具體為：首先對行為附件的狀態空間進行描述，接下來運用Z模式的操作模式對行為附件的狀態遷移進行描述。

所述基于進程演算對AADL進行擴充，為AADL添加并發、不確定以及動作約束算子的形式化描述具體為：定義并發算子、標號遷移系統、并發算子的操作語義、動作約束算子、動作約束算子的操作語義、不確定選擇算子、動作約束算子的操作語義。

本發明采用以上技術方案與現有技術相比，具有以下技術效果：

本發明結合CPS中具體的實例對提出的建模方法進行說明和可行性分析。面向CPS對AADL建模元素進行擴充，提出一種面向CPS的建模規范—— CPS-AADL，為后續模型的形式化驗證，獲得高可靠性的系統模型，開發大規模復雜、安全可靠的CPS系統打下堅實的基礎。

附圖說明

以下將結合附圖對本發明作進一步說明：

圖1為本發明基于AADL的面向CPS的建模方法流程圖；

圖2為飛行導航系統示意圖；

圖3為飛行導航系統的模式邏輯圖；

圖4為飛行導航系統的頂層CPS-AADL模型圖；

圖5為FGS系統構件的CPS-AADL模型。

具體實施方式

本發明的實施提供一種基于AADL的面向CPS的建模方法，為使本領域技術人員更好地理解本發明的技術方案，下面結合附圖和具體實施方式對本發明作進一步詳細描述。通過參考附圖描述的實施方式是示例性的，僅用于解釋本發明，而不能解釋為對本發明的限制。

本發明結合CPS系統的特點，提出一種基于AADL的面向CPS的形式化建模方法。

一、建模與驗證框架