[發明專利]最小不滿足樹制導的混成系統可達性分析方法

有效

• 申請號: 201310146921.4
• 申請日: 2013-04-24
• 公開（公告）號: CN103279488A
• 公開（公告）日: 2013-09-04
• 發明（設計）人: 解定寶;卜磊;李宣東
• 申請（專利權）人: 南京大學
• 主分類號: G06F17/30
• 分類號: G06F17/30
• 代理公司: 南京瑞弘專利商標事務所(普通合伙) 32249
• 代理人: 陳建和

技術領域

本發明涉及混成系統的可達性分析領域，具體而言涉及一種最小不滿足樹制導的混成系統的可達性分析方法。

背景技術

混成系統(hybrid?system)是一類同時具有離散和連續行為特征的復雜系統。在現實生活中,特別是航天、軍工、機械制造等嵌入式相關領域,混成系統均以核心控制器的形式大量存在，并發揮著至關重要的作用。因此,該系統的正確性驗證就有著特別重要的現實意義。當前,相關科研工作者主要采用混成自動機(hybrid?automata)來為混成系統建模。一個混成自動機的運行既包含狀態的離散變化，又包含狀態的連續變化,因此,相應的模型檢驗問題十分困難。例如,即使是混成自動機的一個相對簡單的子類—線性混成自動機(linear?hybrid?automata)，它的可達性問題也已被證明是不可判定的。

傳統的線性混成自動機驗證工具大都使用多面體計算來判定系統相應的可達狀態集，但該方法的指數級復雜度大大限制了其所能解決問題的規模，只能適用于小規模系統.,因而與實際應用需求尚有很大的距離。

近年來，作為基于BDD(binary?decision?diagram)的符號化模型檢驗的一種補充方法，有界模型檢驗(bounded?model?checking,簡稱BMC)技術被提出并得到了廣泛的應用。其基本思想是，將模型行為步數通過整數k來限制，然后將系統k步內的行為進行編碼求解。但是，由于該方法需要在檢驗前將系統k步內所有行為編碼成一個約束集，當問題規模，如給定步長大小、系統變量數目、自動機組合內成員數目等增長后，約束集大小將快速增長，從而導致相應內存需求急劇上升，進而限制了可解決問題的規模。除此以外，雖然線性混成系統的可達性問題可以通過一定的編碼方式使用SMT方法加以解決，但是編碼本身是一項非常復雜的工作，目前沒有任何相應的支撐工具來完成此項工作。對于混成系統的設計和建模工程師而言，如果沒有進行相關長期培訓的話，將相應線性混成自動機模型轉換成SMT問題將會是一項非常困難且極易出錯的工作。

發明內容

針對現有技術的缺陷和不足，本發明的目的在于提供一種混成系統的可達性分析方法，利用最小不滿足樹規避不可達路徑片段，減少對混成系統的圖結構進行深度優先搜索的時間。

為達成上述目的，本發明提出一種混成系統的可達性分析方法，尤其是一種最小不滿足樹制導的混成系統可達性分析方法，包括以下步驟：

步驟1：解析混成自動機，生成該自動機的圖結構；

步驟2：在混成自動機的圖結構上，從初始節點開始做深度優先搜索，在每遍歷一個節點前，對已遍歷的路徑與以該節點為根的最小不滿足樹進行匹配，如果匹配成功，則不遍歷該節點并回溯至另外的節點進行深度優先搜索，否則遍歷該節點并根據目標節點遍歷出一條到達目標節點的目標路徑；

步驟3：根據混成自動機的語義對遍歷出的目標路徑進行編碼，形成一組線性約束；

步驟4：調用線性規劃求解器對該組線性約束進行求解，如果可解則輸出該路徑作為結果，否則轉步驟5；

步驟5：由線性規劃求解器給出該組線性約束的不可約不可解集合（IIS），根據混成自動機的語義，將該組線性約束的不可約不可解集合（IIS）映射成一條不可達路徑；

步驟6：將步驟5得出的不可達路徑插入到以該不可達路徑的最后一個節點為根的最小不滿足樹上，轉步驟2并以該不可達路徑的倒數第二個節點作為初始節點開始做深度優先搜索。

進一步，前述方法更包含如下步驟：設置深度優先搜索的遍歷路徑的長度閥值，深度優先搜索允許重復訪問一個節點且遍歷路徑的長度不超過該長度閥值。

進一步，前述步驟1包含如下步驟：提取混成自動機各節點之間的關系，并用鄰接表來表示自動機的圖結構。

由以上技術方案可知，本發明的混成系統的可達性分析方法，利用最小不滿足樹在搜索到達目標節點的路徑時及早地規避不可達路徑片段，減少搜索路徑的時間，提高路徑搜索的效率。具體來說，本發明的方法具有如下的有益效果：

1、本發明的基于最小不滿足樹制導的混成系統可達性分析方法和一般的目標制導的可達性分析方法相比，當不可達路徑片段離目標節點較遠或不可達路徑片段數量較多時，本方法的效率較一般的方法有極大地提升。

2、本發明所述的最小不滿足樹是以某個節點結尾的所有最小不滿足路徑片段的集合，利用最小不滿足樹可以極大地提高路徑匹配的效率。

附圖說明

圖1為混成系統的可達性分析方法的流程示意圖。