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

在審

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

本發明公開了一種基于模型檢測的反例故障定位方法，主要用于解決使用聲明性語言編寫的模型中的故障定位問題，包括如下步驟：S1、定義有限狀態機FSM規范，FSM規范定義兩只類型的簽名：State和FSM；S2、構建模型；S3、獲取反例cex和滿意實例sat：輸入帶有違反斷言的模型，使用All Analyzer檢查模型中的斷言NoStopTransition獲取反例ces；然后用sat求解器PSAT找到一個滿足斷言屬性并盡可能接近反例ces的滿意實例sat；S4、實例差異分析Diff Analyzer：確定反例cex和滿意實例sat之間的關系和原子并對差異進行分析；S5、可疑表達式排序：計算布爾節點和關系節點的可疑分數分配給可疑表達式并進行排序。本發明對實例之間的差異進行研究分析，進行反例定位，可以快速有效的對聲明性模型進行故障定位。

技術領域

本發明屬于計算機軟件相關技術領域，具體涉及一種基于模型檢測的反例故障定位方法。

背景技術

故障定位是一個實用的研究課題，可以幫助開發人員識別可能導致程序錯誤的代碼位置。大多數現有的故障定位技術都是為命令式程序(例如C和Java)設計的，并且依賴于分析程序的正確和不正確執行來識別可疑語句。

目前缺乏針對聲明性模型的故障定位技術。FL是目前少有的可對聲明性模型進行故障定位的技術。FL使用“單元測試”來計算模型中未通過這些測試的可疑表達式，該技術需要用戶編寫測試用例，但是這并不通用，也不知道FL需要多少測試用例或者用例必須有多好，該技術才有效。本發明是編寫斷言來描述所需屬性，并讓All Analyzer搜索違反該屬性的潛在反例cex,通過分析比較cex和sat實例之間的差異來查找可疑表達式，從而進行故障定位。

發明內容

本發明要解決的技術問題是針對背景技術的缺陷，提供一種通過編寫斷言來搜索模型中的cex和sat實例，從而分析反例來進行故障定位。

為解決上述技術問題，本發明的實施例提供一種基于模型檢測的反例故障定位方法，包括如下步驟：

S1、定義規范：基于AlloyFL基準，定義有限狀態機FSM規范，FSM規范定義兩只類型的簽名：State和FSM；

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

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

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

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

其中，步驟S1包括如下步驟：

S1.1、根據AlloyFL基準定義FSM規范；

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