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

徐 勇,毋國(guó)慶,袁夢(mèng)霆

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

?

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

徐 勇1,2,毋國(guó)慶1,袁夢(mèng)霆1

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

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

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

1 引言

軟件錯(cuò)誤定位是軟件調(diào)試的第一步,其任務(wù)是找出軟件中引發(fā)軟件失效的程序部分.軟件錯(cuò)誤定位費(fèi)時(shí)、費(fèi)力.研究開(kāi)發(fā)自動(dòng)或半自動(dòng)的軟件錯(cuò)誤定位方法一直是學(xué)術(shù)界關(guān)注的熱點(diǎn)課題.

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

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

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

2 基于MBD的軟件錯(cuò)誤定位

2.1 MBD的基本定義[10]

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

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

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

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

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

定理1 一個(gè)組件集A是DS的一個(gè)診斷當(dāng)且僅當(dāng)A是DS所有沖突集的一個(gè)最小碰集.

2.2 基于MBD的軟件錯(cuò)誤定位

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

(1)

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

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

(2)

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

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

(3)

3 啟發(fā)式實(shí)例

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

表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 修復(fù)符號(hào)與元件之間的對(duì)應(yīng)關(guān)系

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

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

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

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

4.1 基于沖突的歸納Craig插值計(jì)算

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

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

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

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

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

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

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

表3 沖突的Craig插值序列

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

需要注意的是:

(1) Interps(C,π[k])中的歸納Craig插值可能不明顯.例如,在表3中,對(duì)于π[3]中,雖然I2和I3不相同,但是語(yǔ)義等價(jià),屬于歸納Craig插值,因?yàn)楦鶕?jù)表2中的元件3的原來(lái)值可知s09=s08.

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

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

表4 對(duì)于表3,計(jì)算了歸納Craig插值后的插值序列

4.2 沖突中元件的過(guò)濾方法

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

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

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

例如,在表4中,對(duì)于Interps(C,π[2]),I2=NULL,但是C[2]=元件2不能確定為無(wú)相關(guān)元件,因?yàn)閷?duì)于Interps(C,π[3]),元件2是歸納Craig插值I2的起始元件.

4.2.2 無(wú)相關(guān)條件語(yǔ)句元件的過(guò)濾方法

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

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

r=Org(r)[vi‖r]

(4)

值得注意的是,這里只是說(shuō)相對(duì)于失敗輸入β,元件1與程序失效無(wú)關(guān).在利用多個(gè)失敗輸入進(jìn)行錯(cuò)誤定位的情況下,先可以對(duì)于每一個(gè)失敗輸入進(jìn)行條件語(yǔ)句元件的不相關(guān)分析,得到相對(duì)于每一個(gè)失敗輸入的不相關(guān)條件語(yǔ)句元件集,然后,將所有不相關(guān)條件語(yǔ)句元件集進(jìn)行求交集即得到相對(duì)于所有失敗輸入的不相關(guān)條件語(yǔ)句元件集.

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

5 相關(guān)算法

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

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

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

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

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

J={in0,in1,…,inn-1}:一個(gè)失敗輸入集合,總失敗輸入數(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) 無(wú)相關(guān)條件語(yǔ)句元件的過(guò)濾方法

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

算法2 無(wú)相關(guān)條件語(yǔ)句元件的過(guò)濾方法

輸出:Removable :相對(duì)于所有失敗輸入的不相關(guān)條件語(yǔ)句元件集.

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)實(shí)現(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插值元件的過(guò)濾方法

首先調(diào)用ComputeInductiveInterp函數(shù)計(jì)算歸納插值矩陣.考察歸納插值矩陣中的每個(gè)Craig插值序列,對(duì)每個(gè)后繼歸納插值根據(jù)定義10判斷是否分割點(diǎn)處所對(duì)應(yīng)的元件屬于冗余元件,其中IsStartC函數(shù)檢驗(yàn)?zāi)吃欠駥儆谄鹗荚?如算法3所示).

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

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

輸出:完成過(guò)濾操作后的沖突.

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 實(shí)驗(yàn)結(jié)果

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

表5 實(shí)驗(yàn)參數(shù)設(shè)置

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

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

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

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

7 結(jié)語(yǔ)

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

[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]王建峰,魏長(zhǎng)安,盛云龍,等.基于錯(cuò)誤交互集的組合測(cè)試軟件故障定位方法[J].電子學(xué)報(bào),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)符號(hào)化模型檢測(cè)[J].電子學(xué)報(bào),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年生,博士生,主要研究方向?yàn)檐浖こ?、軟件調(diào)試.

E-mail:xyus@whu.edu.cn

毋國(guó)慶 男,1954年生,教授、博士生導(dǎo)師,主要研究領(lǐng)域?yàn)檐浖枨蠊こ?、形式化方?

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；責(zé)任編輯:孫瑤

國(guó)家自然科學(xué)基金(No.91118003,No.61003071)；深圳戰(zhàn)略性新興產(chǎn)業(yè)發(fā)展專(zhuān)項(xiàng)資金(No.JCYJ20120616135936123)；中央高校基本科研業(yè)務(wù)費(fèi)專(zhuān)項(xiàng)資金(No.3101046,No.201121102020006)

TP311

A

0372-2112 (2016)10-2514-08

??學(xué)報(bào)URL:http://www.ejournal.org.cn

10.3969/j.issn.0372-2112.2016.10.033