基于克雷格插值的反例理解方法

黃宏濤, 黃少濱, 陳志遠, 張 濤

(哈爾濱工程大學 計算機科學與技術學院, 哈爾濱 150001)

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

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

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

1 基本定義

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

(1)

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

狀態的交替反映了程序語句執行引起的變量變化, 所以模型檢測的反例通常由狀態序列構成. 因為由反例路徑上的兩個相鄰狀態可在線性時間內確定引起狀態變遷的事件, 所以本文把路徑定義為狀態事件的交替序列. 與文獻[6]僅從反例提供的狀態序列中尋找錯誤原因不同, 本文的反例理解方法是與模型相關的, 因此該方法可以直接把反例理解結果映射到源碼.

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

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

定義3事件序列最弱前置條件計算規則如下.

指派表達式序列：

(2)

(3)

事件序列：

(4)

(5)

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

2 反例理解

2.1 計算最弱前置條件

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

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

(6)

其中:uij表示Eij的賦值表達式;tij表示Eij的賦值目標變量. 由規則3可得Wa(ai,φ)的計算公式為

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

(7)

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

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

(8)

其中gi為ei的守護條件. 由規則5可得ρ關于后置條件φ最弱前置條件的計算公式

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

(9)

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

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

2.2 不一致分析

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

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

1)φ1蘊含ψ；

2)ψ∧φ2不可滿足；

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

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

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

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

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

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

(10)

(11)

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

(12)

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

第二條規則用于解析出現在φ2中的子句, 為

(13)

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

(14)

(15)

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

(16)

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

(17)

(18)

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

(19)

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

(20)

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

3 算法分析

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

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

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

4) 從克雷格插值中謂詞與反例狀態的對應關系確定引起反例失效的事件.

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

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

4 實驗結果

本文實現了一個原型CICU算法用于驗證引入克雷克插值后反例理解算法的時間性能, CICU的輸入為LSVT中的BIC算法在醫療保險信息系統模型上產生的反例及其違反的性質, 插值計算使用了文獻[18]的插值證明器. 實驗環境： 處理器Pentium(R) Dual-Core E5200 2.50 GHz, 內存2 G, 操作系統為Ubuntu 11.04 i386, 程序運行環境NetBeans 6.9.1. 實驗目的是在相同條件下對比使用逐次測試(TITU)和計算插值(CICU)的方法理解反例時的時間性能, 實驗結果列于表1.

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

表1列出了部分實驗結果, 這些實驗結果為分別在每條反例上使用TITU算法和CICU算法進行5次重復實驗得出的數據. 由表1可見, CICU算法的時間性能明顯優于TITU算法, 符合本文對算法的時間性能評價.

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

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

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

[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.