黃宏濤, 黃少濱, 陳志遠(yuǎn), 張 濤

(哈爾濱工程大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院, 哈爾濱 150001)

模型檢測技術(shù)[1]的主要優(yōu)勢是它能在證明模型不滿足給定規(guī)范的同時自動給出反例, 但模型檢測器給出的反例僅反映了模型缺陷的癥狀, 驗(yàn)證者仍需花費(fèi)大量時間和精力理解反例, 以確定產(chǎn)生模型缺陷的原因. 在實(shí)際應(yīng)用中, 模型檢測器給出的反例越來越長, 從反例中分析跡失效的原因已被證明為NP完全問題[2]. 因此, 尋找高效的算法進(jìn)行反例自動理解已成為模型檢測技術(shù)亟待解決的問題.

近年來, 如何從反例中發(fā)現(xiàn)模型缺陷的源頭已引起研究人員的廣泛關(guān)注. 文獻(xiàn)[3-5]給出了自動提取失效原因以簡化程序調(diào)試工作的方法. Beer等[6]提出的反例理解方法把反例中引起規(guī)范失效的部分定義為一組原因, 這些原因在因果關(guān)系模型[7]框架下被標(biāo)記出作為可視化的解釋呈現(xiàn)給用戶, 該方法已應(yīng)用于IBM形式化驗(yàn)證平臺Rulebase PE, 并顯著加速了反例理解的速度. 與基于最小不可滿足核方法[8-9]相比, 基于因果關(guān)系的方法能給出理解反例所需的全部相關(guān)信息, 且這些信息是以單個失效原因集而不是一組原因集的形式給出. 此外, 這種基于因果關(guān)系反例理解方法的應(yīng)用獨(dú)立于各種模型檢測器, 但這種與模型無關(guān)的方法也給從錯誤原因到具體錯誤代碼的映射工作帶來困難.

Jose等[10]把MAX-SAT求解機(jī)每次迭代過程中的不可滿足子句作為潛在錯誤位置, 其增量式SAT求解該方法能顯著降低迭代過程的時間開銷. 由于MAX-SAT的判定是NP完全問題, 且該方法沒有對跡進(jìn)行縮減, 故其僅適合于對規(guī)模較小的反例進(jìn)行理解. Wang等[11]使用基于路徑的語法級最弱前置條件算法輔助反例理解, 該方法從反例中提取一個最小原子命題集作為反例不可行的證明, 這種語法級的證明能通過轉(zhuǎn)換語句直接把反例理解結(jié)果映射到錯誤源碼. 由于最弱前置條件的計(jì)算被約束在單個執(zhí)行路徑上, 且最弱前置條件本身計(jì)算代價較低, 因此這種反例理解方法具有更好的可擴(kuò)展性. 然而, 其不可行最小證明的求解過程需要對公式中所有文字進(jìn)行逐個測試, 每個測試過程都會觸發(fā)一個計(jì)算代價較高的SAT求解過程. 為了提高錯誤原因的提取效率, 本文提出一種利用克雷格插值從初始狀態(tài)與反例最弱前置條件的不一致證明中提取模型失效原因的方法, 該計(jì)算過程能在線性時間內(nèi)完成.

1 基本定義

本文用文獻(xiàn)[12]的方法定義程序： 令V={v1,v2,…,vn}為程序變量集;D1,D2,…,Dn分別為v1,v2,…,vn的數(shù)據(jù)域； Evt為程序中的事件集, 事件e∈Evt是定義在V上的一個條件指派：

(1)

定義1Kripke模型為一個四元組K=(S,→,I,L), 其中:S?D1×D2×…×Dn為狀態(tài)集合,n=V； → ?S×Evt×S為遷移關(guān)系集合, (s1,e,s2)∈→當(dāng)且僅當(dāng)T(s1,e)=s2,e∈Evt,s1,s2∈S,T:S×Evt ?S為狀態(tài)轉(zhuǎn)換函數(shù), 其作用是當(dāng)s1滿足e的守護(hù)條件時,e通過指派動作把s1轉(zhuǎn)換為s2；I?S為初始狀態(tài)集合；L:S? 2AP為標(biāo)記函數(shù),AP為原子命題集合.

狀態(tài)的交替反映了程序語句執(zhí)行引起的變量變化, 所以模型檢測的反例通常由狀態(tài)序列構(gòu)成. 因?yàn)橛煞蠢窂缴系膬蓚€相鄰狀態(tài)可在線性時間內(nèi)確定引起狀態(tài)變遷的事件, 所以本文把路徑定義為狀態(tài)事件的交替序列. 與文獻(xiàn)[6]僅從反例提供的狀態(tài)序列中尋找錯誤原因不同, 本文的反例理解方法是與模型相關(guān)的, 因此該方法可以直接把反例理解結(jié)果映射到源碼.

定義2令K為一個Kripke模型,φ為表示待驗(yàn)證性質(zhì)的邏輯公式, 則K關(guān)于φ的反例是一個狀態(tài)事件的有限交替序列ρ=s0e1s1e2s2…en-1sn-1ensn, 使得T(ei+1,si)=si+1和sn不滿足φ同時成立, 其中: 0≤i

對于反例ρ=s0e1s1e2s2…en-1sn-1ensn, 事件序列e1e2…en刻畫了模型所表示的程序引起ρ中狀態(tài)從s0到sn變遷所執(zhí)行的語句序列. 由于sn不滿足φ, 如果把φ視為程序執(zhí)行片段e1e2…en的后置條件, 則可通過計(jì)算最弱前置條件的方法獲得該程序片段違反φ的一個最小謂詞集, 從而定位產(chǎn)生反例的語句[11]. 下面根據(jù)事件結(jié)構(gòu)給出最弱前置條件計(jì)算規(guī)則.

定義3事件序列最弱前置條件計(jì)算規(guī)則如下.

指派表達(dá)式序列：

(2)

(3)

事件序列：

(4)

(5)

式(2)給出了指派表達(dá)式的賦值規(guī)則, 它沒有前提, 是一條公理, 表示如果程序在執(zhí)行賦值語句x=E后有φ成立, 則程序執(zhí)行x=E前必有φ[E/x]成立,φ[E/x]表示把φ中所有自由出現(xiàn)的x都用E替換后得到的公式, 其中φ是一個公式; 式(3)給出了指派表達(dá)式的復(fù)合規(guī)則, 它表示如果程序語句C1的后置條件和語句C2的前置條件相同, 則程序順序執(zhí)行C1和C2后φ成立, 蘊(yùn)含程序順序執(zhí)行C1和C2前成φ立, 其中φ,η,φ是公式； 式(4)中g(shù)為事件e的守護(hù)條件, 表示若Wa為e指派動作的前置條件, 則g∧Wa為e的前置條件, 該規(guī)則的功能與文獻(xiàn)[11]中assume語句最弱前置條件計(jì)算規(guī)則相同； 式(5)給出了事件復(fù)合規(guī)則, 與式(3)類似, 表示如果事件e1的后置條件與事件e2的前置條件相同, 則e1和e2順序執(zhí)行后W2成立, 蘊(yùn)含e1和e2順序執(zhí)行前W1成立,W,W1,W2為公式. 文獻(xiàn)[13]也使用了計(jì)算最弱前置條件的方法對反例進(jìn)行分析, 但其目的是判定偽反例(判定反例的可行性), 而本文計(jì)算最弱前置條件的目的是分離出蘊(yùn)含模型缺陷的謂詞, 這與文獻(xiàn)[10]中使用MAX-SAT求解機(jī)的目標(biāo)相同.

2 反例理解

2.1 計(jì)算最弱前置條件

給定關(guān)于Kripke模型K與公式φ的反例ρ=s0e1s1e2s2…en-1sn-1ensn, 令We(ei,φ)表示事件ei在后置條件φ下的最弱前置條件,Wa(ai,φ)表示ei的指派動作關(guān)于φ的最弱前置條件, 其中:ai為ei的指派動作;WE(Eij,φ)表示指派表達(dá)式Eij關(guān)于φ的最弱前置條件,Eij為ai中的指派表達(dá)式, 1≤i≤n, 1≤j≤k,k為ai中指派表達(dá)式的個數(shù). 由規(guī)則2可得WE(Eij,φ)的計(jì)算公式為

WE(Eij,φ)=φ[uij/tij],

(6)

其中:uij表示Eij的賦值表達(dá)式;tij表示Eij的賦值目標(biāo)變量. 由規(guī)則3可得Wa(ai,φ)的計(jì)算公式為

Wa(ai,φ)=WE(Ei1,WE(Ei2,WE(Ei3,…,WE(Ei(ki-1),WE(Eiki,φ))))).

(7)

由規(guī)則4可得We(ei,φ)的計(jì)算公式為

We(ei,φ)=gi∧Wa(ai,φ),

(8)

其中g(shù)i為ei的守護(hù)條件. 由規(guī)則5可得ρ關(guān)于后置條件φ最弱前置條件的計(jì)算公式

W(ρ,φ)=We(e1,We(e2,We(e3,…,We(en-1,We(en,φ))))).

(9)

由于反例中僅包含If語句和賦值語句, 不同于包含While語句的情況, 因此, 最弱前置條件計(jì)算過程不需要使用創(chuàng)造性的智力去構(gòu)造不變量, 僅需要使用上推符號進(jìn)行推理, 本質(zhì)上是機(jī)械過程, 可使用程序自動完成.

定理1如果ρ=s0e1s1e2s2…en-1sn-1ensn是Kripke模型K上關(guān)于公式φ的反例, 則有s0不滿足W(ρ,φ).

2.2 不一致分析

定理1表明了初始狀態(tài)和反例最弱前置條件的不一致性, 本文通過從兩者不一致性的證明中計(jì)算克雷格插值分離出反例失效的原因.

定義4給定公式對(φ1,φ2), 且φ1∧φ2不可滿足, 則(φ1,φ2)的插值是一個滿足下列條件的公式ψ:

1)φ1蘊(yùn)含ψ；

2)ψ∧φ2不可滿足；

3)ψ中的符號僅與φ1,φ2的公共符號有關(guān).

這里的符號不包括∧,=等邏輯系統(tǒng)自身擁有的符號. 克雷格插值的一個重要性質(zhì)是它反映了兩個公式不一致的原因[14], 即φ1和φ2的不一致是由ψ導(dǎo)致的. 這是使用克雷格插值進(jìn)行反例理解的基本依據(jù)和目的.

證明： 令atoms(φ)-atoms(WP(ρ,φ))表示出現(xiàn)在φ中但不出現(xiàn)在WP(ρ,φ)中的命題變量個數(shù), 當(dāng)atoms(φ)-atoms(WP(ρ,φ))=0時, 有atoms(φ)?atoms(φ)∩atoms(WP(ρ,φ)), 這種情況下顯然有φ蘊(yùn)含φ, 又由定理1知φ∧WP(ρ,φ)不可滿足, 所以φ本身即為φ和WP(ρ,φ)的插值. 假設(shè)對任意的χ, 當(dāng)atoms(φ)-atoms(WP(ρ,φ))=n時, 存在公式ψ為χ和WP(ρ,φ)的插值, 其中n∈N. 當(dāng)atoms(φ)-atoms(WP(ρ,φ))=n+1時, 令φ′=φ[T/p]∨φ[F/ρ], 其中:p為屬于φ但不屬于WP(ρ,φ)的命題變量;φ[T/p]表示使用T替換φ中所有的p;φ[F/p]表示使用F替換φ中所有的p. 此時,φ蘊(yùn)含φ′, atoms(φ′)-atoms(WP(ρ,φ))=n且φ′∧WP(ρ,φ)不可滿足. 由atoms(φ′)-atoms(WP(ρ,φ))=n且φ′∧WP(ρ,φ)不可滿足知存在公式ψ, 使得φ′蘊(yùn)含ψ且ψ∧WP(ρ,φ)不可滿足, 即ψ為φ′和WP(ρ,φ)的插值, 又由φ蘊(yùn)含φ′及φ′蘊(yùn)含ψ知φ蘊(yùn)含ψ, 因此,ψ是φ和WP(ρ,φ)的插值.

定理2斷言了反映φ與WP(ρ,φ)不一致原因插值的存在性. 因此, 可通過計(jì)算產(chǎn)生反例最弱前置條件與初始狀態(tài)不一致的插值進(jìn)行反例理解, 其優(yōu)勢在于： 在特定證明系統(tǒng)中,ψ能在線性時間內(nèi)從φ∧WP(ρ,φ)的不一致性證明中獲得. 文獻(xiàn)[15]給出了從包含未解釋函數(shù)符號的一階邏輯公式不可滿足證明中產(chǎn)生線性規(guī)模插值的方法及線性時間復(fù)雜度算法, 這為基于克雷格插值的反例理解提供了高效方法. 本文使用插值矢列法[16-17]從不可滿足證明中計(jì)算插值.

定義5令Δ是一個文字集合,Δ↓φ表示Δ中的文字且這些文字中出現(xiàn)的命題變量也出現(xiàn)在φ中,Δ/φ表示Δ中的文字且這些文字中出現(xiàn)的命題變量不出現(xiàn)在φ中.

定義6(φ1,φ2)-〈Δ〉[ψ]是一個插值矢列, 當(dāng)且僅當(dāng)下列條件成立:φ1〈Δ/φ2〉, 并且φ2,ψ〈Δ↓φ2〉,ψφ1且ψφ2. 其中:φ1和φ2表示子句集合;Δ表示文字集合;ψ表示公式; 〈Δ〉表示Δ中包含的文字集合;ψφ1表示ψ中出現(xiàn)的變量都出現(xiàn)在φ1中.ψ是φ1和φ2的插值當(dāng)且僅當(dāng)〈Δ〉為空, 這也是插值矢列推導(dǎo)規(guī)則系統(tǒng)的最終目標(biāo). 用于引入子句的假設(shè)引入規(guī)則為

(10)

(11)

下面給出兩條用于解析子句的插值規(guī)則: 第一條規(guī)則用于解析不出現(xiàn)在φ2中的原子命題, 為

(12)

式(12)中p不出現(xiàn)在φ2中;

第二條規(guī)則用于解析出現(xiàn)在φ2中的子句, 為

(13)

式(13)中p出現(xiàn)在φ2中.

(14)

(15)

使用RES-A規(guī)則解析式(14)和(15)引入的子句:

(16)

使用HYP-B規(guī)則引入φ2中的兩個子句:

(17)

(18)

使用RES-B規(guī)則解析式(17)和(18)引入的子句:

(19)

使用RES-B規(guī)則解析式(16)和(19)的解析結(jié)果:

(20)

因此,q即為φ1和φ2的插值, 它反映了公式不一致的原因, 也是導(dǎo)致反例失效的原因. 有了克雷格插值, 即可通過尋找和插值ψ中謂詞相關(guān)的狀態(tài)定位引起錯誤的事件[11]. 如果反例ρ中的狀態(tài)si滿足ψ, 則si即為導(dǎo)致ρ失效的原因, 而ei直接解釋了ρ遷移到ei的原因. 此外, 定義2給出的反例模型也使得本文給出的反例解釋方法不需要為了避免如數(shù)組等不具備克雷格插值性質(zhì)的量詞無關(guān)理論而附加的額外工作.

3 算法分析

基于克雷格插值的反例理解算法CICU(ρ,φ)步驟如下:

1) 由計(jì)算最弱前置條件給出的方法計(jì)算WP(ρ,φ)；

2) 調(diào)用SAT求解機(jī)給出s0不滿足WP(ρ,φ)的證明P；

4) 從克雷格插值中謂詞與反例狀態(tài)的對應(yīng)關(guān)系確定引起反例失效的事件.

由于在反例狀態(tài)序列中引入了引起狀態(tài)變遷的事件序列, 與文獻(xiàn)[6]中算法相比, CICU(ρ,φ)算法和文獻(xiàn)[11]中算法都能直接把反例解釋結(jié)果映射到引起軟件失效的源碼. 由算法的時間性能可見, 為了獲得產(chǎn)生反例不可行原因的語法級證據(jù), 文獻(xiàn)[11]需要從不可滿足公式中提取不一致謂詞的最小集合, 該計(jì)算過程會對不可行公式中的所有文字進(jìn)行逐個測試, 每次測試會觸發(fā)一個SAT判定過程, 設(shè)SAT判定過程的時間復(fù)雜度為O(NSAT), 不一致公式長度為M, 則其計(jì)算最小不一致謂詞集合的時間復(fù)雜度為O(NSAT×M)； CICU(ρ,φ)算法獲取反例初始狀態(tài)不滿足反例最弱前置條件的證明所需時間復(fù)雜度也為O(NSAT), 而CICU(ρ,φ)算法能在線性時間內(nèi)從P中計(jì)算出克雷格插值, 令O(K)為計(jì)算克雷格插值所需的時間代價, 則CICU(ρ,φ)算法的時間復(fù)雜度為O(NSAT+K).

此外, 由計(jì)算結(jié)果正確性可見, 定理1確保了CICU(ρ,φ)算法的最弱前置條件推導(dǎo)能在有限步內(nèi)計(jì)算出不一致公式, 為算法提取克雷格插值提供了有效輸入, 定理2進(jìn)一步斷言了反例初始狀態(tài)與其最弱前置條件克雷格插值的存在性. 因此, 定理1和定理2能保證CICU(ρ,φ)算法對反例失效原因的理解是正確的, 這與文獻(xiàn)[14]的結(jié)論一致. 由于克雷格插值是不唯一的[14], CICU算法給出的結(jié)果與文獻(xiàn)[9-11]一樣都是近似解. 因此, 使用CICU(ρ,φ)算法和文獻(xiàn)[11]的算法對反例進(jìn)行理解時映射出的錯誤事件集都不完備.

4 實(shí)驗(yàn)結(jié)果

本文實(shí)現(xiàn)了一個原型CICU算法用于驗(yàn)證引入克雷克插值后反例理解算法的時間性能, CICU的輸入為LSVT中的BIC算法在醫(yī)療保險信息系統(tǒng)模型上產(chǎn)生的反例及其違反的性質(zhì), 插值計(jì)算使用了文獻(xiàn)[18]的插值證明器. 實(shí)驗(yàn)環(huán)境： 處理器Pentium(R) Dual-Core E5200 2.50 GHz, 內(nèi)存2 G, 操作系統(tǒng)為Ubuntu 11.04 i386, 程序運(yùn)行環(huán)境NetBeans 6.9.1. 實(shí)驗(yàn)?zāi)康氖窃谙嗤瑮l件下對比使用逐次測試(TITU)和計(jì)算插值(CICU)的方法理解反例時的時間性能, 實(shí)驗(yàn)結(jié)果列于表1.

表1 TITU和CICU反例理解時間性能比較

表1列出了部分實(shí)驗(yàn)結(jié)果, 這些實(shí)驗(yàn)結(jié)果為分別在每條反例上使用TITU算法和CICU算法進(jìn)行5次重復(fù)實(shí)驗(yàn)得出的數(shù)據(jù). 由表1可見, CICU算法的時間性能明顯優(yōu)于TITU算法, 符合本文對算法的時間性能評價.

圖1 公式長度對CICU時間性能的影響Fig.1 Influence of formula length on the time performance of CICU

此外, 兩種算法的時間增長率均有一定程度的波動, 圖1給出了CICU算法時間性能與公式長度變化的曲線. 由圖1可見, 當(dāng)不一致公式長度增加時, CICU算法的時間性能隨之提高; 當(dāng)公式長度減小時, CICU算法時間性能的提高趨勢會相應(yīng)減緩. 導(dǎo)致這種情況的原因是： 當(dāng)公式長度較小時, TITU算法所消耗的時間代價顯著降低, CICU算法相對TITU算法在時間性能上的提升空間也相應(yīng)縮小. 總之, CICU算法時間性能提升的波動趨勢與不一致公式長度變化趨勢基本一致.

綜上可見, 基于克雷格插值的反例理解算法能從反例最弱前置條件與初始狀態(tài)的不一致證明中自動產(chǎn)生插值, 產(chǎn)生的插值是導(dǎo)致反例失效的原因. 本文使用的插值證明器能在線性時間內(nèi)推導(dǎo)出插值, 使反例理解速度得到顯著提升. 實(shí)驗(yàn)結(jié)果表明, CICU算法加快了提取反例失效原因的速度, 具有更好的可擴(kuò)展性, 適用于理解更大規(guī)模的反例. 直接把反例理解結(jié)果映射到錯誤事件也能提高調(diào)試工作效率.

[1] Clarke G O, Emerson E M. Model Checking [M]. Cambridge: MIT Press, 1999.

[2] Ben-David S. Applications of Description Logic and Causality in Model Checking [D]. Waterloo: University of Waterloo, 2009.

[3] Groce A, Chaki S, Kroening D, et al. Error Explanation with Distance Metrics [J]. International Journal on Software Tools for Technology Transfer (STTT), 2006, 8(3): 229-247.

[4] Chechik M, Gurfinkel A. A Framework for Counterexample Generation and Exploration [J]. International Journal on Software Tools for Technology Transfer (STTT), 2007, 9(5): 429-445.

[5] Griesmayer A, Staber S, Bloem R. Automated Fault Localization for C Programs1 [J]. Electronic Notes in Theoretical Computer Science, 2007, 174(4): 95-111.

[6] Beer I, Ben-David S, Chockler H, et al. Explaining Counterexamples Using Causality [C]//Proceedings of the 21st International Conference on Computer Aided Verification. Berlin: Springer-Verlag, 2009: 94-108.

[7] Halpern J Y, Pearl J. Causes and Explanations: A Structural-Model Approach [J]. The British Journal for the Philosophy of Science, 2005, 56(4): 843-887.

[8] Suelflow A, Fey G, Bloem R, et al. Using Unsatisfiable Cores to Debug Multiple Design Errors [C]//Proceedings of the 18th ACM Great Lakes Symposium on VLSI. New York: ACM, 2008: 77-82.

[9] Dershowitz N, Hanna Z, Nadel A. A Scalable Algorithm for Minimal Unsatisfiable Core Extraction [J]. Theory and Applications of Satisfiability Testing-SAT, 2006, 60: 36-41.

[10] Jose M, Majumdar R. Cause Clue Clauses: Error Localization Using Maximum Satisfiability [C]//Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation. New York: ACM, 2011: 437-446.

[11] WANG Chao, YANG Zi-jiang, Ivancic F, et al. Whodunit? Causal Analysis for Counterexamples [C]//Proceedings of the 4th international Conference on Automated Technology for Verification and Analysis. Berlin: Springer-Verlag, 2006: 82-95.

[12] Graf S, Saidi H. Construction of Abstract State Graphs with PVS [C]//Proceeding of the 9th International Conference on Computer Aided Verification. Haifa, Israel: LNCS, 1997: 72-83.

[13] Henzinger T A, Jhala R, Majumdar R, et al. Lazy Abstraction [C]//Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York: ACM, 2002: 58-70.

[14] Craig W. Linear Reasoning. A New Form of the Herbrand-Gentzen Theorem [J]. Journal of Symbolic Logic, 1957, 22(3): 250-268.

[15] McMillan K L. An Interpolating Theorem Prover [J]. Theoretical Computer Science, 2005, 345(1): 101-121.

[16] Henzinger T A, Jhala R, Majumdar R, et al. Abstractions from Proofs [C]//Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York: ACM, 2004: 232-244.

[17] Krajícek J. Interpolation Theorems, Lower Bounds for Proof Systems, and Independence Results for Bounded Arithmetic [J]. Journal of Symbolic Logic, 1997, 62(2): 457-486.

[18] Jhala R, McMillan K L. A Practical and Complete Approach to Predicate Refinement [C]//Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer-Verlag, 2006: 459-473.