[發(fā)明專利]基于資源競爭模型的AADL模型可調(diào)度性驗證方法

有效

• 申請?zhí)枺?/td>: 201510064421.5
• 申請日: 2015-02-09
• 公開（公告）號: CN104598302B
• 公開（公告）日: 2017-10-27
• 發(fā)明（設計）人: 董云衛(wèi);隗立超;童安樂
• 申請（專利權）人: 西北工業(yè)大學
• 主分類號: G06F9/46
• 分類號: G06F9/46
• 代理公司: 西北工業(yè)大學專利中心61204
• 代理人: 王鮮凱

技術領域

本發(fā)明涉及一種AADL模型可調(diào)度性驗證方法，特別涉及一種基于資源競爭模型的AADL模型可調(diào)度性驗證方法。

背景技術

文獻“基于UPPAAL的AADL模型可調(diào)度性驗證.計算機應用,2009,(7)”公開了一種針對AADL模型的可調(diào)度性分析方法。該方法將AADL模型之中的各個構建的時間屬性與狀態(tài)轉換利用時間自動機來描述。通過制定轉換規(guī)則，將AADL模型轉換為時間自動機模型，并使用時間自動機分析工具UPPAAL來進行計算，從而得到AADL模型的可調(diào)度性分析結果。文獻方法通過計算轉化的時間自動機的錯誤狀態(tài)的可達性來判斷AADL模型的可調(diào)度性，但是當AADL模型較為復雜時，轉化為時間自動機的狀態(tài)很龐大，可能造成無法計算或者計算起來十分耗時。因此該方法當需要分析的AADL模型較為復雜時會存在一定的缺陷，計算將十分耗時甚至無法得到結果。

發(fā)明內(nèi)容

為了克服現(xiàn)有AADL模型的可調(diào)度性分析方法耗時長的不足，本發(fā)明提供一種基于資源競爭模型的AADL模型可調(diào)度性驗證方法。該方法對AADL模型進行測試，驗證模型的相關時間屬性滿足可調(diào)度性要求。通過分析AADL架構模型中構件間的交互關系得到線程執(zhí)行順序關系，即同步關系或并發(fā)關系，并根據(jù)這些連接關系生成進程的并發(fā)體集合、線程的干擾集。從而建立系統(tǒng)的可調(diào)度性分析模型—資源競爭模型。在此基礎上，將線程構件的執(zhí)行時間屬性以及利用資源競爭模型計算得到的響應時間相加，并與線程構件的截止時間屬性相比較從而得到系統(tǒng)中各個構件的可調(diào)度性，進而分析整個系統(tǒng)的可調(diào)度性。避免了利用自動機模型時遇到復雜系統(tǒng)會造成狀態(tài)過多難以計算的問題，對于結構復雜的AADL模型可以在短時間內(nèi)計算出系統(tǒng)的可調(diào)度性分析結果。

本發(fā)明解決其技術問題所采用的技術方案：一種基于資源競爭模型的AADL模型可調(diào)度性驗證方法，其特點是包括以下步驟：

步驟一、通過分析AADL模型的架構，提取構件與時間相關的屬性以及構件連接關系，找到系統(tǒng)中各個進程的并發(fā)體的集合，系統(tǒng)的并發(fā)體集合用CS表示。

步驟二、通過分析AADL模型的架構，提取構件與時間相關的屬性以及構件連接關系，找到系統(tǒng)的線程干擾集集合，用InterS表示。為每個進程建立完并發(fā)體集合后，針對進程P_i中的任意一個線程T_i^j，建立其干擾集Inter_i^j：

1)分析與線程T_i^j在同一個進程中的線程：如果線程T_i^v和線程T_i^j是并發(fā)關系，即T_i^vCT_i^j，并且線程T_i^v的優(yōu)先級不低于線程T_i^j，那么T_i^v屬于T_i^j的并發(fā)集，即通過分析進程P_i中的每個線程，建立線程T_i^j的并發(fā)集

2)分析與線程T_i^j在不同進程中的線程：對于與線程T_i^j不在同一個進程中的線程，即P_l中的線程，其中l(wèi)≠i，選擇進程P_l中線程執(zhí)行時間之和最大的并發(fā)體，把這個并發(fā)體中的線程加入線程T_i^j的干擾集Inter_i^j中，作為進程P_l(l≠i)中的線程的代表。在計算各個并發(fā)體中線程執(zhí)行時間之和之前，需要針對下面兩種情況對并發(fā)體進行裁剪：

i.并發(fā)體中有線程通過進程連接而與線程T_i^j形成連接關系；

ii.并發(fā)體中有線程的優(yōu)先級低于線程T_i^j。