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

有效

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

本發明公開了基于Prolog的AADL行為模型時間一致性驗證方法，屬于軟件工程的技術領域。本發明在AADL行為附件的基礎上進行擴展以建立帶有時間約束的AADL行為模型，AADL行為模型描述了節點狀態信息、時間約束信息，節點狀態信息能夠定性描述實時系統的屬性，時間約束能夠定量描述實時系統的時間區間，為完整驗證實時系統時間一致性奠定了基礎，將AADL行為模型分解得到的執行路徑轉換為Prolog事實，將形式化描述的隱式時間約束以及顯式時間約束轉換為Prolog規則，利用Prolog規則刻畫實時系統的一致性，即可實現實時系統時間一致性的完整驗證。

技術領域

本發明公開了基于Prolog的AADL行為模型時間一致性驗證方法，屬于軟件工程的技術領域。

背景技術

隨著通信、微電子等技術的飛速發展，嵌入式實時系統廣泛應用于汽車、航空航天等任務關鍵領域中，為了保證實時系統的安全性及可靠性，基于模型驅動架構(Modeldriven architecture，MDA)思想的體系結構分析與設計語言AADL被廣泛的應用到實時系統的建模及驗證中。實時系統的復雜性逐漸增加，隨之AADL規范及附件內容也在不斷的擴展，圍繞其展開的模型驗證工作也成為了熱點。在系統開發的早期階段，就對系統模型的時間一致性、安全性等方面進行驗證，可以避免開發階段時對模型進行反復的修改，大大提高開發的效率。基于邏輯程序語言Prolog，借助SWI-Prolog工具對實時系統行為模型的時間一致性進行前期的驗證是一種可行的方法。

AADL行為模型是對AADL標準語言所構建模型的進一步精化，是以AADL的行為附件為基礎、描述AADL標準組件內部詳細行為的模型。國內的胡凱等人采用時間抽象自動機對實時系統進行建模分析，給出了AADL子集和TASM的抽象語法，并基于語義函數和類ML的元語言形式定義轉換規則，并在此基礎上對實時系統的隱式時間約束進行驗證，但對于時間區間并沒有做詳細驗證；倪水妹通過將帶時間約束的MARTE轉化為基于連續時間的ZIA，實現了在相對低的特征空間維度上有效的對帶時間約束的實時系統的驗證，并刻畫出系統的節點狀態信息及系統時間數據方面的屬性。國外的Maciel P、Andrade E在實時系統建模階段采用Petri網，其具有圖形化描述、精確的語義和強大的表達能力，但Petri網具有很高的空間復雜度，若為了降低復雜度限制Petri網有界，則會降低其表達能力。現有技術中鮮有將實時系統的時間約束和狀態信息統一表述在驗證方法中，存在實時系統時間一致性驗證不完整的缺陷。

發明內容

本發明的發明目的是針對上述背景技術的不足，提供了基于Prolog的AADL行為模型時間一致性驗證方法，對實時系統的狀態信息和隱式時間約束信息及顯式時間約束進行了形式化描述，使用邏輯編程語言Prolog較為完整地驗證了實時系統的一致性，解決了現有技術中對實時系統時間一致性的驗證不夠完整、實時系統模型的表達能力不佳的技術問題。

本發明為實現上述發明目的采用如下技術方案：

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

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

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

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

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

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