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

有效

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

1.一種最小不滿足樹制導的混成系統可達性分析方法，其特征在于，包括以下步驟：

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

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

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

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

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

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

2.根據權利要求1所述的最小不滿足樹制導的混成系統可達性分析方法，其特征在于，前述方法更包含如下步驟：設置深度優先搜索的遍歷路徑的長度閥值，深度優先搜索允許重復訪問一個節點且遍歷路徑的長度不超過該長度閥值。

3.根據權利要求1所述的最小不滿足樹制導的混成系統可達性分析方法，其特征在于，前述步驟1包含如下步驟：提取混成自動機各節點之間的關系，并用鄰接表來表示混成自動機的圖結構。