[發明專利]基于Prolog的AADL行為模型時間一致性驗證方法

有效

• 申請號: 201610654797.6
• 申請日: 2016-08-11
• 公開（公告）號: CN106325855B
• 公開（公告）日: 2019-07-23
• 發明（設計）人: 周勇;劉驍;謝紅梅
• 申請（專利權）人: 南京航空航天大學
• 主分類號: G06F8/20
• 分類號: G06F8/20;G06F8/30
• 代理公司: 南京經緯專利商標代理有限公司 32200
• 代理人: 熊玉瑋

1.基于Prolog的AADL行為模型時間一致性驗證方法，其特征在于，包括如下步驟：

A、建立包含隱式時間約束和顯式時間約束的AADL行為模型，形式化描述AADL行為模型的隱式時間約束和顯式時間約束：

采用邏輯表達式：形式化描述AADL行為模型的隱式時間約束，采用表達式：MinT1＝(a+c)≤E(n)-S(n)≤MaxT1＝(b+d)，及，MinT2≤E(n_i)-S(n_i)+……+E(n_i+j)-S(n_i+j)+……+E(n_k)-S(n_k)≤MaxT2形式化描述AADL行為模型的顯式時間約束，

其中，LB為控制流，n_i、n_k為AADL行為模型中的活動節點i、活動節點k，P為控制流LB走到活動節點i的前置條件，Q為控制流LB走到活動節點k的前置條件，表示邏輯蘊含，@表示時序算子，∧表示邏輯與運算，MaxT1、MinT1為AADL行為模型中任意活動節點n本身持續時間的上下限，S(n)為活動節點n的開始時刻，S(n)∈[a,b]，b、a為活動節點n開始時刻的上下限，E(n)為活動節點n的結束時刻，E(n)∈[c,d]，d、c為活動節點n結束時刻的上下限，MaxT2、MinT2為AADL行為模型中活動節點i、活動節點k之間時間距離的上下限，S(n_i)、E(n_i)為活動節點i的開始時刻、結束時刻，n_i+j為經過活動節點i和活動節點k的路徑上處于活動節點i和活動節點k之間的活動節點i+j，S(n_i+j)、E(n_i+j)為活動節點i+j的開始時刻、結束時刻，S(n_k)、E(n_k)為活動節點k的開始時刻、結束時刻；

B、將步驟A建立的AADL行為模型分解為僅包含活動節點的執行路徑集合；

C、將步驟B中所述執行路徑中活動節點及時間約束轉換為Prolog事實；

D、借助步驟C所述Prolog事實將步驟A中形式化描述后的隱式時間約束和顯式時間約束轉換為Prolog規則；

E、結合步驟C所述Prolog事實及步驟D所述Prolog規則對實時系統的時間一致性進行驗證。

2.根據權利要求1所述基于Prolog的AADL行為模型時間一致性驗證方法，其特征在于，步驟A所述包含隱式時間約束和顯式時間約束的AADL行為模型為一多元組B，B＝(N,Γ,τ,∑,Υ,E,C)，N表示AADL行為模型中所有節點的集合，Γ表示包含活動節點、事件節點、或元素和與元素的節點類型集合，τ表示為AADL行為模型中的節點標注類型的函數，∑表示包含初始態、完成態、返回態、緊急態和復合態的節點狀態集合，γ表示為AADL行為模型中的節點標注狀態的函數，E表示AADL行為模型中節點之間邊的集合，C表示包含隱式時間約束和顯式時間約束的時間約束集合。

3.根據權利要求1所述基于Prolog的AADL行為模型時間一致性驗證方法，其特征在于，步驟B采用如下方法將步驟A建立的AADL行為模型分解為僅包含活動節點的執行路徑集合：

對于事件節點不做處理，

直接將活動節點添加至執行路徑，

獲取當前或元素節點后的各分支的活動節點集合，將各分支的活動節點集合分別添加至后繼節點是當前或元素節點的路徑中，

根據當前與元素節點相鄰活動節點的最短開始時間、最長開始時間、最短結束時間、最長結束時間建立新的活動節點，將新建立的活動節點添加至后繼節點為當前與元素節點的路徑中。