[發明專利]一種不確定性環境下混成AADL模型量化分析方法

有效

• 申請號: 201610223650.1
• 申請日: 2016-04-12
• 公開（公告）號: CN107291435B
• 公開（公告）日: 2020-08-25
• 發明（設計）人: 陳銘松;鮑勇翔
• 申請（專利權）人: 華東師范大學
• 主分類號: G06F8/35
• 分類號: G06F8/35
• 代理公司: 上海麥其知識產權代理事務所(普通合伙) 31257
• 代理人: 董紅曼

本發明提出了一種不確定性環境下混成AADL模型量化分析方法，包括以下步驟：步驟一：利用不確定性附屬語言描述模型中的不確定性；步驟二：利用JAVA類描述源語言AADL的元模型，所述元模型包含混成附屬語言和嵌入式行為附屬語言以描述混成AADL模型；步驟三：將混成AADL模型轉換為NPTA模型，并利用UPPAAL?SMC對所述NPTA模型進行量化分析。本發明通過對混成AADL模型在不確定性環境下轉換成UPPAAL模型，和對UPPAAL模型的量化分析可以得到原模型的量化性質，從而可以在早期混成系統設計的時候及時發現錯誤，降低在不確定性環境中運行可能產生的錯誤。

技術領域

本發明屬于計算機領域，尤其涉及一種不確定性環境下混成AADL模型量化分析方法。

背景技術

本方法基于模型轉換方法，針對混成系統中所用到的混成AADL模型，包括混成附屬語言(Hybrid Annex)、嵌入式系統軟件行為附屬語言(BLESS Annex)和不確定性附屬語言(Uncertainty Annex)，分別使用混成附屬語言轉換方法、嵌入式系統軟件行為附屬語言轉換方法、不確定性附屬語言轉換方法，將混成AADL模型轉換為UPPAAL模型。

元模型(meta model)是用來定義語義模型的構造和規則的,通常稱為定義表達模型的語言的模型。元模型往往用來在某一特定的領域定義一個基礎的通用的語言，來討論和描述該領域的問題及解決方法。特別是在軟件工程領域中對模型的分析和構建非常適用。

模型轉換方法(Model Transformation)是一種自動化的方法確保一系列模型的一致性，是模型驅動開發方法(Model Driven Development)的核心思想。它通過對一系列模型不同的分析與驗證，可以系統設計的早期階段獲得更多的性質。這樣有助于保證系統的質量屬性，并有效控制開發時間與成本。它通常需要輸入源模型和對應的元模型，并通過轉換規則生成指定的模型。

體系結構分析與設計語言AADL(Architecture AnalysisDesign Language)是一種字符化和圖形化的語言,由SAE(Society for Automotive Engineers)體系結構描述語言附屬委員會、嵌入式計算系統委員會、航空電子系統公司共同提出,用于設計和分析性能關鍵的實時系統的軟硬件體系結構。且AADL可以通過擴展支持更多的應用,這樣的擴展可以被定義為核心標準的一個Annex部分。開源AADL工具集環境(OSATE)是AADL建模的一個工具,它基于Eclipse框架,包含文本、XML和圖形編輯器以及眾多分析工具。這些工具都是開源Eclipse插件,可以進行擴展。

價格時間自動機(PTA,即Priced Timed Automata)與傳統的時間自動機不同,它的時鐘能夠以不同速率進行變化.通過將不同PTA的輸入和輸出進行組合,可以組成價格時間自動機網絡(NPTA,即Networks of Priced Timed Automata).NPTA中的價格時間自動機通過廣播信道和共享變量進行同步。

在基于模型檢測的方法下，傳統的混成AADL模型分析有以下不足：

1.沒有考慮到混成建模的AADL子集，一般的模型分析僅僅包括AADL模型中的核心語義，而不包括混成(Hybird)和行為(BLESS)的描述語義。不能準確(Uncertainty)的描述需要和物理環境頻繁交互的系統。

2.沒有不確定性描述語義，由于缺乏不確定性描述語義，便無法進行不確定性分析。

3.傳統的混成AADL模型分析只能給出某一系統性質是否滿足，不能給出某一系統性質有多大概率滿足，因此不能更進一步分析系統安全等性質。

發明內容