徐 勇,毋國慶,袁夢霆

(1.武漢大學計算機學院,湖北武漢 430072；2.廣東肇慶學院數(shù)學與統(tǒng)計學院,廣東肇慶526061)

?

結(jié)合Craig插值分析的軟件錯誤診斷方法

徐 勇1,2,毋國慶1,袁夢霆1

(1.武漢大學計算機學院,湖北武漢 430072；2.廣東肇慶學院數(shù)學與統(tǒng)計學院,廣東肇慶526061)

基于模型診斷(MBD)的理論應用到軟件錯誤定位中取得了一定的效果.但是經(jīng)典MBD理論基于元件間獨立地發(fā)生故障這一假設,導致軟件錯誤定位的結(jié)果中存在假陽性的診斷.論文對現(xiàn)有基于MBD 的軟件錯誤定位方法進行了改進,提出了沖突中元件的冗余分析方法.該方法既包括了基于Craig插值的元件冗余分析機制,同時利用條件語句取值的二元性(真或假)的特點,對沖突中的條件語句元件進行軟件錯誤的無相關分析.實驗結(jié)果表明:沖突中的元件冗余分析方法可以有效地減少診斷的假陽性率,將診斷結(jié)果數(shù)減少了48.4%,碰集樹生成的結(jié)點數(shù)減少了47.6%.

基于模型診斷；軟件錯誤定位；冗余分析；Craig 插值

1 引言

軟件錯誤定位是軟件調(diào)試的第一步,其任務是找出軟件中引發(fā)軟件失效的程序部分.軟件錯誤定位費時、費力.研究開發(fā)自動或半自動的軟件錯誤定位方法一直是學術界關注的熱點課題.

近年來的文獻資料顯示,人們對于自動軟件錯誤定位方法展開了大量而深入的研究[1-5].在這些研究工作中,其采用的技術方法主要可分以下幾類:(1) 基于頻譜的錯誤定位方法[1-2]；(2) 基于模型診斷(Model-Based Diagnosis)的軟件錯誤定位方法[3,4]；(3) 基于概率統(tǒng)計方法的軟件錯誤定位[5].當然,也有將值替換[6],狀態(tài)比較[7],程序不變式[8],測試用例分析[9]等應用到軟件錯誤定位中.本文關注的是基于MBD的軟件錯誤定位.

針對電器元件中的故障診斷問題,Retier[10]提出MBD理論和診斷方法.其基本思想是,用合適的邏輯(例如一階邏輯等)構(gòu)造系統(tǒng)的行為和結(jié)構(gòu)模型,通過系統(tǒng)運行行為與系統(tǒng)預期行為之間的不一致的觀察,結(jié)合邏輯的推理功能推導出哪個或哪些元件引發(fā)了系統(tǒng)工作異常；診斷的計算依賴于沖突集及碰集樹(Hit Set Tree)的構(gòu)造,每一個診斷都是沖突集的最小碰集.如果將程序中的語句視為MBD中的元件,可以將 MBD應用于軟件的錯誤定位[11-13].但是程序中的語句之間往往存在著數(shù)據(jù)及控制依賴關系,而Reiter在其MBD理論中假設了系統(tǒng)中的元件獨立地發(fā)生功能故障.因此,直接應用MBD到軟件的錯誤定位而不考慮元件之間存在的依賴關系將會影響錯誤診斷的準確性,即候選診斷中存在假陽性.

Birgit Hofer[13]等人提出應用程序切片獲得語句間的依賴關系,并與MBD相結(jié)合提高診斷結(jié)果的質(zhì)量.Jorg Weber[14]等人則提出增加元件依賴關系模型來表達元件之間可能發(fā)生故障的關系,從而支持對元件依賴性故障和獨立性故障的診斷.MBD中沖突的存在是系統(tǒng)中的元件集導致系統(tǒng)的行為模型與實際行為的不一致,也即是邏輯上的不可滿足.Craig插值提供了一種更簡單的形式展示不可滿足公式的原因[15].借助Craig插值,可以分析出沖突中的元件在系統(tǒng)行為模型邏輯上不可滿足的作用,從而識別出冗余元件.與此同時,程序中條件語句的取值無非是真和假.而給定一個具體失敗輸入,其只可能執(zhí)行程序的某一條路徑.如果沖突中的條件語句元件無論是取真或假值,系統(tǒng)的合法行為模型仍不可滿足,則表明沖突中的條件語句元件與當前失敗輸入所引發(fā)的軟件失效是不相關的.事實上,文獻中既有利用Craig插值對不可滿足的邏輯公式進行化簡分析的成功應用[16-17],也有利用分支條件語句取值二元性的特點進行程序錯誤定位[18-19],這些都啟發(fā)我們在MBD框架下存在進行沖突中元件不相關分析的可能性.

2 基于MBD的軟件錯誤定位

2.1 MBD的基本定義[10]

定義 1 一個診斷系統(tǒng)DS是三元組(SD,CMP,OBS),其中SD表示系統(tǒng)描述；CMP是有限整數(shù)集合,表示系統(tǒng)中的元件；OBS表示系統(tǒng)行為的觀察.其中SD和OBS一般用一階句子集表示.

定義 2 對某個元件c(c∈CMP),謂詞AB(c)表示其異常工作,而AB(c)則表示其正常工作.

定義3 一個組件集C是一個沖突當且僅當C?CMP且{SD∪OBS}∪{AB(c)|c∈CMP}是不可滿足的.

定義4 一個組件集Δ是一個診斷當且僅當Δ?CMP且{SD∪OBS}∪{AB(c)|c∈CMPΔ}是一致的.

更進一步,Reiter提出診斷計算方法,即有如下定理:

定理1 一個組件集A是DS的一個診斷當且僅當A是DS所有沖突集的一個最小碰集.

2.2 基于MBD的軟件錯誤定位

Robert Konighofer[3]等開發(fā)了一款基于MBD的程序錯誤定位和修復工具Forensic.Forensic以運行失效的程序及其規(guī)約作為輸入,其中程序的規(guī)約既可以是程序斷言,也可以是正確的參考程序,并且將程序中賦值語句的右值和條件語句視為元件.假設原失效程序為P,Forensic的錯誤定位由以下幾個步驟來完成:

(1)

其中i表示輸入符號向量,r是由cmp函數(shù)返回的一組不確定值,也稱為修復符號向量.同時,在程序分析過程中,無論正確或失效的執(zhí)行路徑,對路徑條件用約束求解得到一組輸入值.

(3)診斷的計算.沖突的計算依賴Repair函數(shù),其定義如下.

(2)

其中,R={r|CmpOf(r)∈Q},Q是元件的集合.

定義5 元件集Δ是P的一個診斷當且僅當Repair(CMPΔ)=true；元件集C(C?CMP)是P的一個沖突當且僅當Repair(C)=false.

(3)

3 啟發(fā)式實例

圖1中的程序P是運行失效的,其中第4行的語句是錯誤的,應該是“res=y”.Forensic首先通過程序預處理識別出所有的元件集CMP={0,1,2,4,5,6},元件1,4是條件語句,而其他元件屬于賦值語句的右值.然后,通過符號執(zhí)行得到π[i‖r](表1)和一失敗輸入β={x=0,y=1,z=0}.表2列出了修復符號與其元件間的對應關系.最后,Forensic計算診斷即是構(gòu)造碰集樹的過程.Forensic首先從給定的輸入β利用Repair′計算出一個沖突C1={1,2,3,4,6}(圖2中的結(jié)點n0).根據(jù)沖突C1中的元件,以寬度優(yōu)先,從左到右的順序擴展分支和結(jié)點,最終得到一個指定深度的碰集樹(圖2所示).碰集樹中的結(jié)點分為三類:(1) 用√ 標記的結(jié)點,它表示計算出的一個診斷；(2) 用×標記的結(jié)點為剪枝結(jié)點；(3) 內(nèi)部結(jié)點,對應一個沖突.

表1 路徑條件約束 π[i‖r]

π[k]ks15≥s02∧s15≥s01∧s15≥s00∧s14=0∧s07=00s16≥s02∧s16≥s01∧s16≥s00∧s14!=0∧s07=01s11≥s02∧s11≥s01∧s11≥s00∧s10=0∧s07!=02s12≥s02∧s12≥s01∧s12≥s00∧s10!=0∧s07!=03

表2 修復符號與元件之間的對應關系

修復符號CmpOf(r)Org(r)s060xs071y>xs082xs09,s133max(x,y)s10,s144two>zs11,s155twos12,s166z

圖2中給出最后診斷結(jié)果,即5個診斷,其中3個診斷的基是1,2個診斷的基是2.顯然,除了第1個診斷以外,其他的診斷都屬于假陽性.如本文引言所述,程序中的語句間往往存在數(shù)據(jù)與控制流依賴的,而MBD中診斷的計算是依賴于沖突的概念.但是沖突的概念并沒有體現(xiàn)沖突中元件之間的依賴關系.根據(jù)定義5,沖突的存在即意味著公式不可滿足.而Craig插值提供了一種更簡單的形式展示兩個公式不可滿足的原因.因此存在著可能利用Craig插值表示形式去識別沖突中不相關的元件.例如,對于表1中第3條路徑條件(k=3),對于沖突C1的兩次分割點{{1,2},{3,4,6}},{{1,2,3},{4,6}},其對應的Craig插值是s08≤ 0,s09≤ 0,而這兩個邏輯公式是語義等價的.這表明,元件3的執(zhí)行與否不影響該條路徑條件的不可滿足性,即元件3是冗余的.圖1中程序也反映到這一點,給定失敗輸入β,程序中第9行的賦值語句的值實際是來自第3行語句的值.

另一方面,程序中條件語句的取值非真即假.如果當某個條件語句無論取真或取假值都無法消除軟件的失效,則可以認為該條件語句對于該軟件運行失效是無相關.例如,對于表1中的π[3],元件4屬于條件語句,所對應的分支約束條件是two>z.那么當前的失敗輸入β無論元件4取真或假,π[i‖r]仍然不可滿足,即程序運行失效仍舊存在.因此,元件4是與當前失敗輸入軟件失效無關的元件.

4 MBD的沖突中元件冗余分析

4.1 基于沖突的歸納Craig插值計算

定義6 Craig插值[15].給定公式φ1和φ2,如果φ1∧φ2是不可滿足,則φ1和φ2的插值ψ有以下性質(zhì):(1)φ1|=ψ,(2)ψ∧φ2是不可滿足的,(3)ψ中的符號僅與φ1和φ2中的符號有關.

為了敘述方便,引入一些符號.用Interp(φ1,φ2)表示邏輯公式φ1,φ2的Craig插值.用J表示測試用例集作為輸入來進行錯誤診斷,且|J|=1.用π[k]表示π[i‖r]中某條路徑條件,顯然,若路徑條件集合PASS且n=|PASS|,則k={0,1,…,n-1}.表1列出了圖1中的程序所有合法的路徑條件即π[i‖r].

沖突是元件的集合,為了對沖突中的元件進行冗余分析,必須先將沖突映射成路徑條件中的邏輯公式.根據(jù)式(3),給定一沖突和失敗輸入集,最終一定可以獲得一組不可滿足的邏輯公式.首先,我們定義函數(shù)RepairSym,其將元件編號映射到修復符號.而Sym函數(shù)是將元件集合Q映射到的修復符號集合,即Sym(Q)=∪RepairSym(c),(c∈Q).顯然,給定一個元件集和某路徑條件,可以誘導出一個邏輯合取式,形式化描述如下.

定義7 給定一元件集Q和π[k](π[k]=T1∧T2∧…∧Tn),其中Ti為路徑條件中的約束條件.則令Γ(Q,π[k])=∧Ti,其中Ti來自π[k]中的子句且Ti中使用了Sym(Q)中變量符號.

設沖突C={c1,c2,…,cn}和π[k],假設沖突中的元件是有序的.用F1,i,Fi+1,n表示沖突C可以分割成兩個沖突子集,其中i的取值是1,2,…,n-1(i也稱為分割點).對于每個分割點,就可以得到兩個公式A=Γ(F1,i,π[k]),B=Γ(Fi+1,n,π[k]),且A∧B=⊥.令Ii=Interp(A,B),就可以構(gòu)造一個Craig插值序列.

定義8 沖突的Craig插值序列.給定沖突C={c1,c2,…,cn}和π[k].Interps(C,π[k])={I1,I2,…,Ii,In-1}是C相對于π[k]的插值序列,其中i∈{1,2,…,n-1},且Ii=Interp(Γ(F1,i,π[k]),Γ(Fi+1,n,π[k])).

顯然,計算出π[i‖r]中的每條π[k]路徑條件的Craig插值序列,就可以得到一個Craig插值矩陣.表3列出的是圖2中沖突{1,2,3,4,6}的Craig插值矩陣,其中,對于π[k],若Ii=false,則后繼的Craig插值省略了,用“-”表示.在沖突中多個連續(xù)的分割點處,若存在語義等價(用符號“≡”表示)的Craig插值,則稱為歸納Craig 插值.歸納Craig插值的存在表明在該分割點處所對應的元件的執(zhí)行與否不影響π[k]不可滿足,即可能存在冗余元件.

表3 沖突的Craig插值序列

定義 9 給定沖突C和π[k],設有Craig插值序列Interps(C,π[k])={I1,I2,…,Ii,In-1}.對于C的連續(xù)分割點i,j(j>i),若有Ii≡Ij,則稱Ii對于分割點i,j是歸納Craig插值.

需要注意的是:

(1) Interps(C,π[k])中的歸納Craig插值可能不明顯.例如,在表3中,對于π[3]中,雖然I2和I3不相同,但是語義等價,屬于歸納Craig插值,因為根據(jù)表2中的元件3的原來值可知s09=s08.

(2) 歸納Craig插值具有傳遞性,即Ii≡Ii+1且Ii+1≡Ii+2,則Ii≡Ii+2.因此,對于多個連續(xù)的歸納Craig插值,除第一個以外的插值稱為后繼歸納Craig插值,用特殊值NULL標記(如表4).并且稱第一個歸納Craig插值在沖突分割點所對應的元件為歸納Craig插值的起始元件.

(3) 對于Craig插值矩陣中的每個Interps(C,π[k])進行歸納插值計算后,就得到歸納Craig插值矩陣(表4).

表4 對于表3,計算了歸納Craig插值后的插值序列

4.2 沖突中元件的過濾方法

4.2.1 基于歸納Craig插值元件的過濾方法

給定沖突C、歸納Craig插值矩陣M,若Interps(C,π[k])∈M中存在后繼歸納Craig插值Ii時(即Ii=NULL),則沖突分割點i所對應的元件(用C[i]表示)可能為冗余元件.換言之,若Ii=NULL,刪除沖突中的元件C[i]不會影響π[k]的不可滿足性.但是刪除元件C[i]可能會影響到其他路徑條件π[s](s≠k)的不可滿足性.因此必須給出條件判定后繼歸納Craig插值所對應的元件是否為無相關冗余元件.

定義 10 給定沖突C={c1,c2,…,cn}和歸納Craig插值序列矩陣M,令Interps(C,π[k])= {I1,I2,…,Ii,In-1}∈M,若Ii=NULL且C[i]屬于冗余元件,當且僅當對于Interps(C,π[s])(s≠k),C[i]不屬于其中歸納插值的起始元件.

例如,在表4中,對于Interps(C,π[2]),I2=NULL,但是C[2]=元件2不能確定為無相關元件,因為對于Interps(C,π[3]),元件2是歸納Craig插值I2的起始元件.

4.2.2 無相關條件語句元件的過濾方法

考慮到給定具體的失敗輸入,其只能執(zhí)行π[i‖r]中的某一條路徑條件,且該路徑條件的不可滿足是違反程序合法行為模型造成的,而其他的路徑條件的不可滿足是因為其中的條件語句元件的分支約束不滿足造成的.稱路徑條件中的條件語句元件的分支約束不滿足的路徑條件為非執(zhí)行路徑條件.下面的定義則給出了根據(jù)沖突的Craig插值序列識別非執(zhí)行路徑條件的方法.

定義11 設有沖突C={c1,c2,…,cn},π[i‖r],失敗輸入和Craig插值序列矩陣.對于某π[k],如果存在Craig插值Ii=false且C[i]為條件語句元件,則稱π[k]對應于元件C[i]的非執(zhí)行路徑條件.

r=Org(r)[vi‖r]

(4)

值得注意的是,這里只是說相對于失敗輸入β,元件1與程序失效無關.在利用多個失敗輸入進行錯誤定位的情況下,先可以對于每一個失敗輸入進行條件語句元件的不相關分析,得到相對于每一個失敗輸入的不相關條件語句元件集,然后,將所有不相關條件語句元件集進行求交集即得到相對于所有失敗輸入的不相關條件語句元件集.

圖3是將本文提出的沖突冗余元件分析方法應用到圖1的過程所生成的碰集樹.與Forensic的診斷結(jié)果相比較,診斷數(shù)從5個減少到2個,碰集樹中的結(jié)點數(shù)從9個減少到3個.

5 相關算法

將上一節(jié)的思想表述成沖突元件過濾算法,該算法可以分三個步驟:

(1) 計算Craig插值序列矩陣數(shù)組

給定一個失敗輸入、沖突和π[i‖r],利用ComputeInterMatrix函數(shù)計算Craig插值序列矩陣.計算完所有失敗輸入所對應的插值序列矩陣就得到Craig插值序列矩陣數(shù)組.如算法1所示.

算法1 計算Craig插值序矩陣數(shù)組

輸入:C={c0,c1,…,cn-1}:一個沖突,其中元件個數(shù)|C|

J={in0,in1,…,inn-1}:一個失敗輸入集合,總失敗輸入數(shù)|J|

π[i‖r]:程序合法行為模型,總的路徑條件數(shù)|PASS|

輸出:Craig插值序列的矩陣數(shù)組G

1. fors= 0;s< |J|;s++do

2. G[s] ← ComputeInterMatrix(π[i‖r],C,ini)

3. end for

(2) 無相關條件語句元件的過濾方法

對于算法1產(chǎn)生的每一個Craig插值序列矩陣,調(diào)用ComputeNEPath函數(shù)找出非執(zhí)行路徑條件集NE(K,c).對NE中的路徑條件進行條件變更后利用Sat函數(shù)進行驗證元件c對于當前失敗輸入是否屬于無相關條件語句元件.所有的失敗輸入所對應的無相關條件語句元件的交集就是可以過濾的條件語句元件.具體內(nèi)容見算法2.

算法2 無相關條件語句元件的過濾方法

輸出:Removable :相對于所有失敗輸入的不相關條件語句元件集.

1. Removable ←φ

2. fori= 0;i< |J|;i++ do

3. Removed ←φ

4. NE(K,ci) ← ComputeNEPath(G[i],C) //ci∈C

5. 將NE中的π[k](k∈K)實現(xiàn)條件變更得到π′[k]

7.Removed←Removed∪ ci

8.endif

9.ifRemovable= φthen

10.Removable←Removed

11.else

12.Removable←Removable∩Removed

13.endif

14.endfor

(3)基于歸納Craig插值元件的過濾方法

首先調(diào)用ComputeInductiveInterp函數(shù)計算歸納插值矩陣.考察歸納插值矩陣中的每個Craig插值序列,對每個后繼歸納插值根據(jù)定義10判斷是否分割點處所對應的元件屬于冗余元件,其中IsStartC函數(shù)檢驗某元件是否屬于起始元件(如算法3所示).

顯然,算法中的基本操作是可滿足性計算或者計算Craig插值,則算法3的時間復雜度最大.而算法3在最壞情況下復雜度約為O(|PASS‖C‖J|),這也是整個算法時間復雜度.

算法3 基于歸納Craig插值元件的過濾方法

輸出:完成過濾操作后的沖突.

1. fori= 0;i< |J|;i++ do

2. M [i] ← ComputeInductiveInterp(G[i])

3. end for

4. fori= 0;i< |J|;i++ do

5. for eachI=Interps(C,π[k])∈M [i]

6. forz=0;z<|C|-1;z++ do

7. ifIz=NULL and IsStartC(C[z])=false then

8. Removable ← Removable∪C[z]

9. end if

10. end for

11. end for

12. end for

13. return C-Removable

6 實驗結(jié)果

為了驗證本文方法(記PA)的有效性,在Forensic中實現(xiàn)了PA算法.采用Tcas的38個錯誤版本(Tcas有41個錯誤版本,但其他幾個版本Forensic無法計算出診斷)作為實驗對象將PA與Forensic進行比較研究.實驗參數(shù)設置列在表5.表6列出了將PA與原Forensic方法應用到Tcas進行錯誤定位產(chǎn)生的診斷結(jié)果(對版本號v8,v16,v19,syb-ce-it分別設置為 200,400,200).從診斷總數(shù)來看,Forensic總體計算出254個診斷,而PA計算出131個診斷,診斷數(shù)減少了48.4%,其中,單元件診斷數(shù)減少率為22.9%,雙元件診斷數(shù)減少率為66.4%.

表5 實驗參數(shù)設置

表6 Forensic與PA診斷結(jié)果的比較

采用Forensic方法,在診斷的計算過程中碰集樹總體生成647個結(jié)點,而PA總體生成339個結(jié)點,結(jié)點的減少率為47.6%(圖4).從平均數(shù)來看,原Forensic方法診斷計算平均生成17個結(jié)點,而本文方法平均生成9個結(jié)點.

從診斷計算時間開銷來看(圖5),Forensic診斷計算總的時間花費是64.8s,而PA診斷計算花費是418.1s.顯然,本文所提方法花費在診斷計算的時間是原Forensic方法的大約6倍.造成診斷計算時間增多的原因多次調(diào)用Z3進行Craig插值計算與可滿足性判定.

將syb-dia-ni參數(shù)取1和2時,對診斷數(shù)的差值進行比較(圖6),顯然,與Forensic相比,PA增加該參數(shù)的取值對診斷的診斷準確度的影響較小,也即是敏感度低于Forensic.

7 結(jié)語

本文分析了MBD軟件錯誤定位中診斷假陽性的一些原因,并提出了一種沖突中冗余元件的分析方法.該方法既利用歸納的Craig插值去識別沖突中的冗余元件,同時能夠清除無相關條件語句元件.實驗結(jié)果表明該方法能夠通過消除沖突的無相關元件,從而減少診斷的假陽性.下一步工作包括:更廣泛地對本文所提方法進行實證研究.進一步結(jié)合其方法(比如基于統(tǒng)計錯誤定位方法,多層次的MBD診斷方法)對基于MBD軟件錯誤定位方法進行優(yōu)化改進.

[1]Lee Naish,Hua Jie Lee,Kotagiri Ramamohanarao.A model for spectra-based software diagnosis [J].ACM Transactions on software engineering and methodology (TOSEM) ,2011,20(3):11.

[2]Rui Abreu,Peter Zoeteweij,Rob Golsteijn,Arjan J C Van Gemund.A practical evaluation of spectrum-based fault localization [J].Journal of Systems and Software,2009,82(11):1780-1792.

[3]Konighofer R,Roderick Bloem.Automated error localization and correction for imperative programs [A].Formal Methods in Computer-Aided Design (FMCAD) [C].USA:IEEE,2011,91-100.

[4]Rui Abreu,Arjan J C Van Gemund.Diagnosing multiple intermittent failures using maximum likelihood estimation [J].Artificial Intelligence,2010,174(18):1481-1497.

[5]Chao Liu,Long Fei,Xifeng Yan,Jiawei Han,Samuel P Midkiff.Statistical debugging:A hypothesis testing-based approach [J].IEEE Transactions on Software Engineering,2006,32(10):831-848.

[6]Dennis Jeffrey,R Gupta.Effective and efficient localization of multiple faults using value replacement [A].IEEE International Conference on Software Maintenance [C].USA:IEEE,2009.221-230.

[7]Andreas Zeller,Ralf Hildebrandt.Simplifying and isolating failure-inducing input [J].IEEE Transactions on Software Engineering,2002,28(2):183-200.

[8]Swarup Kumar Sahoo,John Criswell,Chase Geigle,Vikram Adve.Using likely invariants for automated software fault localization [J].ACM SIGARCH Computer Architecture News,2013,41(1):139-152.

[9]王建峰,魏長安,盛云龍,等.基于錯誤交互集的組合測試軟件故障定位方法[J].電子學報,2014,42(6):1173-1178.

WANG Jian-feng,WEI Chang-an,et al.Locating errors in combinatorial testing using set of possible faulty interactions [J].Acta Electronica Sinica,2014,42(6):1173-1178.(in Chinese)

[10]Raymond Reiter.A theory of diagnosis from first principles [J].Artificial intelligence,1987,32(1):57-95.

[11]Rui Abreu,Peter Zoeteweij,Arjan J C van Gemund.An observation-based model for fault localization [A].Proceedings of the International Workshop on Dynamic Analysis [C].USA:ACM,2008.64-70.

[12]Franz Wotawa,Mihai Nica,Iulia Moraru.Automated debugging based on a constraint model of the program and a test case [J].The Journal of Logic and Algebraic Programming,2012,81(4):390-407.

[13]Birgit Hofer,Franz Wotawa.Combining slicing and constraint solving for better debugging:The conbas approach [A].Advances in Software Engineering [C].Hindawi Publishing Corporation,2012.Article ID 628571.

[14]Jorg Weber, Franz Wotawa.Diagnosing dependent failures in the hardware and software of mobile autonomous robots [A].New Trends in Applied Artificial Intelligence [C].Berlin:Springer,2007.633-643.

[15]William Craig.Linear reasoning.a new form of the herbrand-gentzen theorem [J].The Journal of Symbolic Logic,1957,22(3):250-268.

[16]Evren Ermis,Martin Schaf,Thomas Wies.Error invariants [A].Lecture Notes in Computer Science:Formal Methods (Volume 7436) [C].Berlin:Springer,2012.187-201.

[17]陳祖希,徐中偉,霍偉偉,等.基于 Craig 插值的線性混成系統(tǒng)符號化模型檢測[J].電子學報,2014,42(7):1338-1346.

CHEN Zu-xi,XU Zhong-wei,et al.Symbolic model checking for linear hybrid systems base on craig interpolation [J].Acta Electronica Sinica,2014,42(7):1338-1346.(in Chinese)

[18]Xiangyu Zhang,Neelam Gupta,Rajiv Gupta.Locating faults through automated predicate switching [A].Proceedings of the 28th International Conference on Software Engineering [C].USA:ACM,2006.272-281.

[19]Jurgen Christ,Evren Ermis,Martin Schaf,Thomas Wies.Flow-sensitive fault localization [A].Verification,Model Checking,and Abstract Interpretation [C].Brelin:Springer,2013.189-208.

[20]Leonardo De Moura,Nikolaj Bj?rner.Z3:An efficient smt solver [A].Tools and Algorithms for the Construction and Analysis of Systems [C].Berlin:Springer,2008.337-340.

徐 勇 男,1977年生,博士生,主要研究方向為軟件工程、軟件調(diào)試.

E-mail:xyus@whu.edu.cn

毋國慶 男,1954年生,教授、博士生導師,主要研究領域為軟件需求工程、形式化方法.

E-mail:wgq@whu.edu.cn

Software Fault Localization Based on Model-Based Diagnosis Combined Craig Interpolant Analysis

XU Yong1,2,WU Guo-qing1,YUAN Meng-ting1

(1.ComputerSchool,WuhanUniversity,Wuhan,Hubei430072,China;2.SchoolofMathematicsandStatistics,ZhaoqingUniversity,Zhaoqing,Guangdong526061,China)

Model-based diagnosis,an intelligent diagnosis theory has been successfully applied in software fault localization with promising results.However,traditional MBD relies on the assumption that components in the system fail dependently which makes the diagnoses with high false positives in software fault localization.In this paper,a component redundancy analysis approach is presented.The approach not only uses Craig interpolant to filter redundant components,but also employs a fact that a branch predicate evaluates to either true or false to filter some branch condition components.Experimental results show that the proposed approach effectively reduces the false positive rates of diagnoses,i.e.,reducing the number of diagnosis by 48.4%,and reducing the number of nodes of hitting set tree generated during diagnosis computation by 47.6%.

model-based diagnosis (MBD); fault localization; redundancy analysis; Craig interpolant

2015-11-03；

2016-02-16；責任編輯:孫瑤

國家自然科學基金(No.91118003,No.61003071)；深圳戰(zhàn)略性新興產(chǎn)業(yè)發(fā)展專項資金(No.JCYJ20120616135936123)；中央高?；究蒲袠I(yè)務費專項資金(No.3101046,No.201121102020006)

TP311

A

0372-2112 (2016)10-2514-08

??學報URL:http://www.ejournal.org.cn

10.3969/j.issn.0372-2112.2016.10.033