[發(fā)明專利]一種基于模型檢測的反例故障定位方法

在審

• 申請?zhí)枺?/td>: 202210583746.4
• 申請日: 2022-05-25
• 公開（公告）號: CN114936109A
• 公開（公告）日: 2022-08-23
• 發(fā)明（設計）人: 程實;詹廣生;李治賢;王浩任;吳佳駿;高欣欣;于夢;文萬志
• 申請（專利權）人: 南通大學
• 主分類號: G06F11/07
• 分類號: G06F11/07;G06F9/448
• 代理公司: 南通一恒專利商標代理事務所(普通合伙) 32553
• 代理人: 梁金娟

1.一種基于模型檢測的反例故障定位方法，其特征在于：包括如下步驟：

S1、定義規(guī)范：基于AlloyFL基準，定義有限狀態(tài)機FSM規(guī)范，F(xiàn)SM規(guī)范定義兩只類型的簽名：State和FSM；

S2、構建模型：包括違反斷言NoStopTransition的三個部分：類型簽名、表示約束的公式和調用All Analyzer的命令；

S3、獲取反例cex和滿意實例sat：輸入帶有違反斷言的模型，使用All Analyzer檢查模型中的斷言NoStopTransition獲取反例ces；然后用sat求解器PSAT找到一個滿足斷言屬性并盡可能接近反例ces的滿意實例sat；

S4、實例差異分析Diff Analyzer：確定反例cex和滿意實例sat之間不同的關系和原子并對差異進行分析；

S5、可疑表達式排序：計算布爾節(jié)點和關系節(jié)點的可疑分數(shù)分配給可疑表達式并進行排序。

2.根據(jù)權利要求1所述的基于模型檢測的反例故障定位方法，其特征在于：步驟S1包括如下步驟：

S1.1、根據(jù)AlloyFL基準定義FSM規(guī)范；

S1.2、FSM規(guī)范定義了兩種類型的簽名：State和FSM，并定義State的字段sig State、FSM的字段one sig FSM；

S1.3、FSM規(guī)范包括三個事實fact段落，表達約束。

3.根據(jù)權利要求1所述的基于模型檢測的反例故障定位方法，其特征在于：步驟S2包括如下步驟：

S2.1、模型包括違反斷言NoStopTransition的三個部分：類型簽名、表示約束的公式和調用All Analyzer的命令；

S2.2、類型簽名sig用來表示基本數(shù)據(jù)類型，并且字段捕獲這些數(shù)據(jù)類型之間的關系；

S2.3、表示約束的公式包括事實fact、謂詞pred和斷言NoStopTransition，表示對數(shù)據(jù)類型的約束；

S2.4、調用All Analyzer的命令包括run和check，其中，run表示查找令人滿意的滿意實例sat，check用于查找違反斷言屬性的反例cex；

S2.5、將搜索實例的任務轉換為布爾公式，并使用sat求解器來檢查公式的可滿足性；每個關系的每個值都被轉換為布爾公式中的不同變量。

4.根據(jù)權利要求1所述的獲取cex和sat實例，其特征在于：步驟S3包括如下步驟：

S3.1、將帶有違反斷言的模型轉換為邏輯公式輸入模型處理工具NvSMV；

S3.2、使用All Analyzer搜索違反斷言的潛在反例cex；

S3.2.1、通過編譯得到字節(jié)碼文件BcFile，檢查字節(jié)碼文件BcFile；去掉與檢驗性質無關和與狀態(tài)遷移無關的語句，在字節(jié)碼文件BcFile中多個字節(jié)碼指令對應內存中的一個狀態(tài)改變；

S3.2.2、斷言NoStopTransition表示屬性，該屬性在模型的所有實例中保持；

S3.2.3、使用斷言NoStopTransition檢查stop State是否表現(xiàn)為接收器，AllAnalyzer通過生成一個反例cex來反駁這一斷言；

S3.3、使用sat求解器PSAT找到一個滿足斷言屬性并盡可能接近反例cex的滿意實例sat；

S3.3.1、運用模型處理工具NvSMV將輸入模型轉換為表示硬約束的邏輯公式，并將來自反例cex的信息轉換為表示軟約束的公式；

S3.3.2、將實例查找問題轉化為部分最大sat問題，然后使用Pards解算器找到滿足所有硬約束和盡可能多的軟約束的公式；

S3.3.3、使用sat求解器PSAT來查找滿足斷言屬性且與cex相似的滿意實例sat。