基于謂詞抽象的測試用例約簡生成方法

郭曦，張煥國,2

(1. 武漢大學 計算機學院，湖北 武漢 430072；2. 武漢大學 空天信息安全與可信計算教育部重點實驗室，湖北 武漢 430072)

1 引言

軟件開發是一個不斷迭代和演化的過程，需要頻繁地進行測試，同時測試用例集的規模隨著測試需求的變更在不斷地增大，此時不可避免地存在冗余的測試用例，即測試用例集的某個子集也滿足所有的測試需求。由于測試用例在設計和維護等階段均有較大開銷，因而在滿足測試需求的基礎上，有必要生成約簡的測試用例集，其目標是設計并使用一組數量較少的測試用例滿足給定的測試需求，在提高軟件測試效率的同時降低測試成本。

目前，測試用例約簡[1]的方法是：首先針對每個測試需求生成對應的測試用例，所有測試需求對應的測試用例組成初始的測試用例集；再使用啟發式方法、整數規劃方法等對這個初始的測試用例集進行約簡，去掉冗余的測試用例。這種方法的缺點在于它的效果取決于最初選定的測試用例集，不能完全實現根據測試目標對測試用例集的整體優化。此外，與測試用例集約簡相關的測試用例集的錯誤檢測效率問題也引起研究人員的關注，先后提出了多種測試用例優先級技術，以提高測試用例集的錯誤檢測效率。

軟件系統狀態空間的大小和對應的測試用例集的數量有直接關系，最壞情況下，軟件系統的狀態空間和系統的規模呈指數關系。在測試過程中，往往因為模型的狀態空間爆炸問題而難以產生精簡的測試用例集，從而影響對軟件系統所具有的性質的驗證效率。謂詞抽象是一類特殊的屬性保持的抽象方法，是解決或者緩解狀態空間爆炸最有效的方法之一[2]，謂詞在原始模型的狀態空間上定義了一個等價關系，通過狀態集合之間的映射，把原始模型轉換成為一個易于處理的、包含有限狀態的抽象模型。在抽象模型中成立的性質，在原始模型中也成立，而在抽象模型中不能證明真偽的性質，在原始模型中可能成立，也可能不成立。在測試用例生成階段，通常利用謂詞抽象自動驗證工具的反例抽象精化功能：為了生成滿足某個性質p的測試用例，在程序中檢驗p?的滿足情況，若出現反例，則表明可以生成滿足p的測試用例；若找不出反例，則表明沒有測試用例與p對應。

針對大規模軟件系統狀態遷移數量龐大，容易導致狀態空間爆炸，從而難以生成精簡的測試用例集對軟件系統所具有的性質進行驗證的問題，本文以系統狀態的遷移作為研究對象，提出一種基于謂詞抽象的測試用例約簡生成方法。首先通過謂詞在原始系統的狀態空間上定義等價關系，得到狀態約簡的抽象模型；然后基于抽象模型的狀態遷移關系，給出針對每個等價類的測試用例約簡生成算法，從而在降低原始模型狀態冗余的情況下生成約簡的測試用例集。

2 相關工作及存在的問題

對于軟件系統M，設其測試目標是由m個測試需求組成的集合R={r1, r2,…,rm}，同時對每個測試需求生成n個測試用例集T={t1, t2,…,tn}。現有的測試用例集約簡方法通過尋找T的某個子集，用盡可能少的測試用例滿足測試需求集R。可以證明，測試用例集的約簡是一個NP-C問題[3]，故一般采用啟發式算法來獲得近似解。

Chvatal等人提出貪心（greedy）算法（G算法）來求解測試用例集約簡問題[4]，它每次從測試用例集T中選擇一條測試用例，使它能最大程度上滿足測試需求集R中未被滿足的需求，然后從R中刪除這些已被滿足的需求，直到所有的需求都被滿足,最壞情況下，該算法的時間復雜度為O( mn·min(m, n))。

Harrold提出了一種啟發式方法[1]，它根據測試用例的重要性來選擇測試用例（HGS算法）。對于測試需求Ri和Rj，如果i＜j，則該算法認為在重要程度上，Ri對應的測試用例比Rj對應的測試用例要高。該方法首先將測試需求r1, r2,…,rm劃分到集合R1, R2,…,Rk( k≤n)中，其中Ri( i=1,2,…,k )為所有被T中i個測試用例所滿足的測試需求，即首先選出集合R1對應的測試用例，然后使用貪心算法選擇滿足R2的測試用例，直到R2對應的測試需求均被滿足，再依次處理集合中剩下的測試需求，最壞情況下，該算法的時間復雜度為O( m( m+n) k)。

Chen等人在貪心算法的基礎上提出GE算法和GRE算法[5]。GE算法使用必不可少策略挑選出初始的測試用例集，再通過貪心算法對其進行約簡，其時間復雜度仍為O( mn·min(m, n))。GRE算法循環交替使用1-1冗余策略以及必不可少策略生成初始測試用例集，再通過貪心算法選擇其他的測試用例以滿足剩下的測試需求。最壞情況下，GRE算法的時間復雜度為O(min(m, n)( m+n2k))，k表示一個測試用例最多能滿足的測試需求的個數。

Lee等人提出的整數規劃方法[6]將最小代表集的選擇問題轉換為整數規劃問題，在理論上可以生成滿足R的最優測試用例集，但該算法的運算開銷呈指數級增長，計算復雜性也較高。

以上這幾種算法都是針對測試用例集的簡化策略，章曉芳等[7]在上述方法的基礎上提出一種對測試需求進行約簡的測試用例集優化方法，通過建立測試用例集和測試需求集之間的映射，判斷是否存在一個測試用例滿足多個測試需求的情況。程亮等[8]結合安全操作系統的對測試的需求，提出了簡并測試集，設計基于安全狀態轉移的測試集生成方法。

目前，現有的測試用例集約簡方法中，基于系統的狀態空間約簡的研究較少。徐明迪等[9]采用標記變遷系統對可信計算平臺信任鏈進行測試，從易測性對信任鏈的狀態進行描述并對系統的動作進行約簡，為測試用例構造方法提供了理論依據。本文在其基礎上，進一步以軟件系統的狀態遷移作為研究對象，通過謂詞抽象的方法對軟件系統的初始狀態集合進行等價類劃分，這樣可以有效地減少系統狀態集合內部的冗余和后續約簡計算的工作量，并依據等價的抽象狀態集合以及抽象狀態遷移關系生成約簡的測試用例集，提高對軟件系統所具有的性質進行驗證的效率。

3 系統模型狀態約簡與等價類的問題求解

對于一個軟件系統，理想的測試用例集是在滿足測試需求的基礎上，用例的數量要盡可能少。現有的二叉判定圖和樹型結構等約簡測試用例的方法，都是以系統所能達到的狀態作為操作對象。實際上，決定測試用例集規模的直接因素往往不是系統的狀態數量，而是狀態遷移的數量。

為了更好地表示軟件系統的狀態以及狀態間的遷移關系，通過謂詞抽象技術，使用謂詞表示軟件系統的狀態變遷，可以有效地對大規模軟件系統的狀態進行約簡。謂詞抽象使用一組有限數量的謂詞把系統表示為有限狀態機模型，該模型就是對原始系統的一種抽象，它較原始系統有更小的狀態集合，其中每一種狀態屬于一個等價類，每個等價類里面包含若干個滿足謂詞劃分的原始狀態。本節還證明了一個基于原始模型系統狀態空間的問題：經過等價類劃分后得到若干個子問題，其中每個等價類對應一個子問題，首先對子問題進行求解，再將各子問題的解組合起來就得到原問題的解，該方法可以用來指導構建基于原始模型的約簡測試用例集。

3.1 抽象狀態的形式化定義

設原始系統模型M的狀態集合為C，初始狀態集合為IC，狀態遷移關系集合為RC，謂詞在狀態集合C上定義一個等價關系，該等價關系把原始模型的初始狀態集合劃分成若干個等價類，每個等價類包含一個或多個狀態，2個狀態等價當且僅當它們屬于同一個等價類。對于一組謂詞Φ=(φ1,φ2,…,φn)，和一組與之對應的布爾變量B=(B1, B2,…,Bn)，使用謂詞公式φ來表示原始模型的狀態C，并使用變量B1, B2,…,Bn上的一組正交布爾表達式來表示對應的抽象模型的狀態集合A。抽象狀態表示為A( B1, B2,…,Bn)，其初始狀態集合記為IA，每個抽象狀態與一個等價類相對應。為了表示模型的原始狀態和抽象狀態之間的關系，給出如下定義。

定義1 抽象算子α把模型的原始狀態φ映射到抽象模型對應的抽象狀態：

定義2 精化算子γ將抽象模型對應的抽象狀態映射到模型的原始狀態：

對于抽象模型的抽象狀態A( B1, B2,…,Bn)，使用謂詞φi替換其中對應的Bi，即可得到該抽象狀態對應的所有原始狀態。由定義1和定義2可知：原始狀態與抽象狀態是一對一的關系，而抽象狀態與原始狀態是一對多的關系。

3.2 基于等價類劃分的問題求解

由于謂詞在原始模型M的狀態集合上定義等價關系，M中每一個狀態屬于一個等價類，而一個等價類是用一個抽象狀態表示，故抽象狀態可以反映出原始模型狀態之間的關系。基于等價類劃分的方法可以將原問題分解為若干個子問題并經過分別求解，劃分后的問題狀態空間遠小于原問題狀態空間，并且若某個子問題無解，則可以確定原問題無解。下面給出原始模型狀態中的等價類定義。

定義3 對于一個基于原始模型的狀態空間問題，若原始狀態集合C依據謂詞集合Φ劃分成了若干個子狀態集合{C1, C2,…,Ck}，稱Ci(1≤i≤k)是C中關于Φ的一個等價類，如果Ci滿足如下條件：

1) Ci是C的一個子集；

2) Ci中每個狀態都同時滿足Φ所對應的一組布爾變量B的取值；

3) Ci中任意一個狀態與jC中任意一個狀態關于Φ所對應的布爾變量B取不同的值，其中i≠j,1≤i, j≤k。

一個原始模型的狀態空間問題的一個等價類就是它的一個子問題，如果狀態集合C中任意一個狀態關于Φ所對應的布爾變量的取值均相同，即原始模型不能劃分出一個以上的等價類，則稱該狀態空間問題為不變等價類，此時系統的狀態不能進行等價類劃分。

定理1 針對一個基于原始模型M的狀態空間問題，如果可以通過謂詞集合Φ劃分為若干個等價類（即子問題），那么這些子問題可以單獨求解，并且這些子問題解的組合就是原問題的解。

證明 由定義1，在抽象算子α運算過程中，系統M的狀態集合C依據謂詞集合Φ進行劃分：{C1, C2,…,Ck}，每個劃分Ci( Ci?C)都是關于Φ的一個等價類，k為等價類的個數，即M的問題Q被分解成若干個子問題{q1, q2,…,qk}。設Ci中的狀態c1和Cj中的狀態c2關于謂詞Φ集合布爾變量B的取值分別為和，根據定義3，≠，即表示一個等價類中的任意狀態對應的布爾變量的真值不會影響到另一個等價類中任意一個狀態對應的布爾變量的真值，那么每個子問題就可以在抽象模型上單獨進行求解。在求得每個子問題解的基礎上，根據定義2，抽象模型中各個子問題，可以通過精化算子γ映射到原始模型，依據謂詞抽象的性質，在抽象模型中成立的性質，在原始模型中也同樣成立，故在抽象模型中所求得的每個子問題的解s，同樣也是原始模型中原問題的解，由于在子問題求解過程中，不同等價類中的狀態之間關于布爾變量B的取值之間不會產生沖突，所以這些子問題的解的組合〈s1, s2,…,sn〉 就是原問題的解。 證畢

定理1表明，一個基于原始模型的狀態空間的測試用例生成問題，可以依據謂詞抽象操作將狀態空間劃分為若干個子問題并單獨求解，若每個子問題都有解，則原問題也有解。經謂詞抽象后，抽象模型擁有較少的狀態空間及狀態遷移關系，此時對每個等價類（子問題）生成約簡的測試用例，最后將各個等價類所生成的測試用例集組合起來，就得到原始模型的約簡測試用例集。

4 測試用例約簡生成方法

通過對原始模型進行謂詞抽象處理，得到約簡的抽象模型，它包含若干原始模型狀態集合上的等價類。在生成測試用例之前，首先需要獲得抽象模型中的狀態遷移集合，作為測試用例生成的基礎，然后對每一個等價類中的狀態集合，生成針對原始系統模型待驗證性質的測試用例，最后依據等價類劃分問題求解的性質，得到針對原始模型的約簡測試用例。

4.1 抽象模型狀態遷移生成算法

基于謂詞的抽象模型的狀態取決于所使用的謂詞集合，狀態遷移關系的復雜程度對測試用例的構造有直接關系，故需要生成抽象狀態的遷移關系，下面給出系統模型M遷移關系的定義及其性質。

定義4 對于一個原始模型的狀態空間集合C及其狀態遷移集合RC，如果有c1∈C, c2∈C ，并且(c1→c2)∈RC ，則稱c1和c2之間存在直接遷移關系。

定義5 對于一個原始模型的狀態空間集合C及其狀態遷移集合RC，如果有c1, c2, c3∈C，并且c1和c2之間、c2和c3之間均存在直接遷移關系，則稱c1和c3之間存在間接遷移關系。

定義6 直接遷移和間接遷移統稱為遷移關系。

遷移關系反映出系統狀態之間的轉換關系以及狀態的可達情況，并能夠指導系統狀態的等價關系的構建。下面給出遷移關系的性質。

性質1 遷移關系具有傳遞性，即如果1c和2c之間、2c和3c之間均存在遷移關系，則1c和3c之間存在遷移關系。

原始模型遷移關系集合RC與抽象模型遷移關系集合RA的關系是：設與初始狀態φ所關聯的抽象狀態是A( B1, B2,…,Bn)，φ對應的原始狀態遷移關系記為，其中Rφ?RC，Rφ是原始狀態φ對應的原始模型狀態遷移關系，則與Tj關聯的抽象模型狀態遷移關系通過如下表達式確定[10]：

其中，pj是Tj的進行語義操作的決定條件，即當前狀態若滿足pj，才存在遷移關系。在抽象遷移關系中，若成立，那么(A( B1, B2,…,Bn))=false，即抽象狀態A( B1, B2,…,Bn)在中無后繼狀態。表示在遷移關系Tj下，當前狀態的后繼狀態。若post[ Tj]成立，則ci的值為Bi；若post[ Tj](A(|))??φi成立，則ci的值為?Bi，若均不成立，則ci的值為true。

在定義了初始狀態集合IC、初始狀態遷移關系集合RC的原始模型后，就可以使用抽象算子α'和求出抽象模型。抽象模型的初始狀態集合為IA，抽象狀態遷移關系集合為RA。算法1給出了抽象遷移關系集合RA的求解過程。

算法1 抽象模型的狀態遷移關系生成算法。

輸入：謂詞集合Φ、原始模型的初始狀態集合IC，狀態遷移關系集合RC。

輸出：相對于謂詞集合Φ的抽象模型A的狀態遷移集合。

1) α' (Φ):=∧{Bi|Φ?φi,1≤i≤n}; //初始化抽象算子α'

2) Ainit:=α'(IC);//初始化A的初始狀態集合

3) Arest:=Ainit; //初始化未處理的抽象狀態

4) Atran:=null; //初始化狀態遷移關系

5) while(Arest不為空)

6) 從Arest中取出一個抽象狀態A'；

9) Atran:=Atran+A'tran;//更新Atran集合

10) Arest:=Arest-{A '};//更新Arest集合

11) end while

12) returnAtran;

4.2 基于狀態約簡的測試用例生成算法

測試用例集的約簡基于模型系統狀態遷移的約簡，原始模型狀態集合依據謂詞集合Φ經算法1得到抽象狀態遷移集合，由于每個抽象狀態對應一個等價類，故以每一個等價類中的狀態遷移集合為研究對象，通過謂詞抽象自動驗證工具對原始模型所具有的性質進行驗證，若不滿足該性質，工具可以自動返回不滿足該性質的程序執行路徑，并以此生成針對每個等價類的測試用例集。依據定理1，把抽象狀態中每個等價類的測試用例組合起來，就可以得到原始模型的約簡測試用例。

本文的測試用例約簡生成方法首先針對每個等價類所生成約簡的測試用例。對于測試用例ti和tj，它們之間存在如下關系。

1) 包含關系：若ti∩tj=ti，則ti包含于tj，記為ti?tj，它表明ti對應的狀態遷移集合包含在tj對應的狀態遷移集合中。

2) 相交關系：若ti∩tj≠?，則ti與tj之間存在交集，記為ti⊕tj，它表明ti和tj有公共的狀態遷移關系。

3) 獨立關系：若ti∩tj=?，則ti與tj相互獨立，記為ti＜＞tj，即ti和tj沒有公共的狀態遷移集合。

其中包含關系是相交關系ti-ti∩tj≠?的特例。在測試用例約簡生成過程中，可以根據以上3種狀態關系對每個等價類中的測試用例集進行約簡，顯然包含關系和相交關系可以約簡，而獨立關系不能進行約簡。其約簡規則如下。

若ti?tj，由于ti對應的狀態遷移集合包含在tj對應的狀態遷移集合之中，故約簡后的結果是ti。

若ti⊕tj，由于ti和tj之間存在部分重合關系，將ti和tj對應的測試用例重合的部分作為約簡后的結果，即保留ti∩tj。

若ti＜＞tj，此時ti和tj之間沒有公共的遷移狀態，此時無法進行約簡操作。

在生成測試用例的時候，由于每個等價類可能對應于原始模型中多個狀態，如果不能生成一條測試用例滿足該等價類中的各種狀態，此時需要將測試用例依據以上3種關系進行約簡，這樣可以在滿足原始模型狀態遷移關系的同時，能夠生成規模較小的測試用例集。

本文是針對原始模型待驗證的性質集合P來生成測試用例的，故需要對這些性質進行形式化描述，作為謂詞抽象自動驗證工具的輸入參數。這里的性質集合P就是謂詞抽象過程中待驗證的原始模型所具有的性質集合。

算法2 每個等價類的測試用例約簡生成算法。

輸入：經形式化描述的待驗證的性質集合P。

輸出：約簡的測試用例集RT。

1) :RTnull=;//初始化約簡的測試用例集

2) :STnull=;//初始化所有測試用例所包含的狀態遷移集合

3) while(P不為空)

4) 從P中選擇一條待驗證的性質p;

5) P:=P-{p};//從集合P中刪除p

6) T:=genTestCase( p);//生成針對p的測試用例T

7) foreachpi∈P( pi≠p)do

8) satisfy( T, pi);//驗證T是否滿足pi

9) end

10) E:=tran( T)∩ST;//生成已包含在之前測試用例所覆蓋的狀態

11) if getSubSuite( E)不為空then

13) foreachT'∈getSubSuite( E)except TLdo

14) ':'TTE=-;//更新'T集合

15) end

16) end

17) ST:=ST+tran( T);//更新ST集合

18) :RTRTT=+;//更新RT集合

19) end while

算法2依據每個等價類中的狀態之間的關系，針對原始模型待驗證的性質，調用謂詞抽象自動驗證工具生成對應的測試用例，并對生成的測試用例集進行約簡。經前面的分析可知，每一個等價類中只有包含關系和相交關系的測試用例可以進行約簡。算法首先從待驗證的性質集合中選取一條性質，通過函數genTestCase( p)調用謂詞抽象自動驗證工具生成針對性質p的測試用例T，并驗證T是否還可以滿足性質集合P中其他的性質，若能夠滿足，則從P刪除對應的性質。函數satisfy( T, pi)用來驗證測試用例是否滿足某些性質。函數tran( T)記錄測試用例所包含的狀態遷移集合，它與ST集合求交集，得出已包含在之前測試用例所覆蓋的狀態E。函數getSubSuite( E)生成包含狀態E的所有測試用例集，并從中選擇包含狀態數最多的測試用例TL，同時刪除其他用例中包含E的部分，并更新ST和RT集合，直到P集合為空。

圖1顯示了對測試用例進行約簡過程，其中圖1(a)表示3個測試用例：t1=〈s0, s1〉,t2=〈s0, s1, s2〉,t3=〈s0, s1, s2, s3〉,它們分別顯示各自所包含的狀態以及狀態遷移關系，依據本節引入的約簡規則，使用算法2可以生成約簡后的測試用例t，如圖1(b)所示，該測試用例t可以替代t1, t2, t3,以減少系統依據測試用例進行測試環境初始化所帶來的開銷。

圖1 測試用例約簡過程

算法復雜性方面，由于算法2是一種基于線性搜索的測試用例約簡方法，對于每條性質所生成的測試用例都需要對P中其他性質進行檢驗，其時間復雜度為O( k)，其中k=|P|，故整個算法的時間復雜度為O( k2)，相對于貪心算法，算法2的時間復雜度較低，效率也更高。需要說明的是，通過謂詞抽象自動驗證工具，該算法可以同時得到P中不能針對謂詞集合Φ生成測試用例的性質，這些性質的來源可能是謂詞抽象自動驗證工具無法為其生成測試用例，也可能是謂詞集合需要進一步精化再來生成該性質的測試用例。

對于每個等價類生成的約簡測試用例集{RT1, RT2,…,RTk}，其中k=|IA|，把RT1, RT2,…,RTk依據算法1得到的抽象狀態遷移關系RA進行連接就可以得到對應于原始模型系統的測試用例集，該集合就是最后約簡的測試用例集。RT1, RT2,…,RTk的連接過程是：設抽象模型的遷移關系為I1→I2→…→Ik，其中k=|IA|，則RT1, RT2,…,RTk依據抽象模型遷移關系構建序列：RT1→RT2→…→RTk，對于RT1→RT2，把RT1中的每條測試用例與RT2中的每條測試用例依據原始狀態遷移關系集合RC進行連接，依次拓展到RTk。

圖2表示2個測試用例的連接過程，設t1∈RT1, t2∈RT2，(s3→s5)∈RC， 測 試 用 例t1=s0, s2, s3,t2=s5, s6, s7，將t1和t2連接所得到的測試用例t=s0, s2, s3, s5, s6, s7。

圖2 不同等價類的測試用例連接過程

4.3 狀態約簡實例分析

本節通過一個實例，對基于謂詞抽象方法的原始模型狀態約簡過程進行描述。對于一個原始模型，設其原始狀態集合C={si|si=i,0≤i ≤14}，狀態遷移關系集合RC為

圖3上部分反映原始狀態及狀態間的遷移關系。謂詞集合Φ為{φ1, φ2, φ3, φ4}，其中φ1=si＜5,φ2=si＜7,φ3=si＞10,φ4=si＞12。與φ1,φ2, φ3,φ4關聯的布爾變量是B1, B2, B3, B4，按照算法1，各狀態相對于謂詞集合Φ的抽象狀態為

此時，抽象模型對應的抽象狀態集合A為

抽象狀態所對應的遷移關系集合：

圖3的下部分顯示了基于謂詞抽象所得到的約簡模型及抽象狀態之間的遷移關系。通過對比，原始模型的狀態經謂詞抽象操作后被劃分成了5個等價類，每個等價類包含多個原始模型的狀態，抽象模型的狀態數量和狀態間的遷移關系的復雜程度均明顯減少。約簡的狀態模型作為測試用例生成的前期處理，有助于生成較小規模的測試用例集。

圖3 謂詞抽象處理前后系統狀態的遷移關系

5 測試用例約簡生成的仿真實驗

為了驗證本文提出的方法的有效性，進行了一系列仿真實驗，把現有的幾種典型的測試用例約簡方法和本文所提出的方法進行對比。實驗環境是2.6.24-24內核的Ubuntu 8.10版Linux系統，2.2GHz的處理器，2GB的物理內存空間。

仿真實驗的方案是：構建原始模型的程序控制流圖（CFG），根據CFG設定初始的謂詞集合；為了驗證原始模型是否所具有待驗證的性質，使用BLAST工具[11]構建基于初始謂詞的抽象模型，并使用定理證明器Simplify[12]對抽象狀態遷移關系進行求解；在獲得抽象模型的狀態遷移關系后，使用本文的算法生成約簡的測試用例；由于測試用例約簡問題是NP-C問題，一般采用啟發式算法獲取近似解，為了對比本文方法的性能，分別使用貪心算法、啟發式算法（HGS算法）和GRE算法這3種典型的測試用例約簡算法進行對比實驗，并分析實驗結果。

仿真實驗過程中涉及到的參數有：程序源代碼的長度L，程序CFG圖中狀態個數S，約簡模型中狀態個數S’，基于本文方法生成的測試用例個數T，通過分析測試對象程序的調用圖（call graph），分別使用N-live和N-dead表示語法上可達與不可達的位置個數，N-prdc表示每個測試對象為滿足待驗證的性質所產生的謂詞個數，每一次實驗就是對一組參數（S, S’, N-prdc ,T）的賦值。

測試對象為kbfiltr、floppy、cdaudio及ping，其中，前3個分別是關于鍵盤、軟驅和音頻的設備驅動程序，ping是一個網絡監測工具。仿真實驗中待驗證的性質為程序的狀態覆蓋，通過生成約簡的測試用例集以滿足該性質。實驗結果如表1所示，其中T-G、T-HGS、T-GRE分別為對測試對象使用貪心算法、啟發式算法和GRE算法所生成的測試用例個數。

實驗結果顯示，貪心算法、HGS算法和GRE算法在測試用例約簡生成方面的性能大致相當，也符合文獻[13]對這幾種算法比較的結果。由于HGS算法和GRE算法在計算過程中，可能會調用貪心算法，故在貪心算法計算過程中通常生成比HGS算法和GRE算法略大的測試用例集。與現有的幾種算法相比，基于謂詞抽象的測試用例約簡生成算法由于對原始模型的狀態依據謂詞進行劃分，能夠得到約簡的抽象模型及其狀態間的遷移關系，表1中T數值表明本文的方法可以在滿足程序待驗證的性質的基礎上，生成數量較少的測試用例集。Ratio顯示本文的方法相對于其他3種方法關于測試用例個數的最大約簡比例，對于規模較小的kbfiltr和ping，測試用例數量的約簡比例較高；而對于規模較大的floppy和cdaudio，則約簡比例相對較低，其原因是隨著程序規模的增大，系統的狀態空間和遷移關系更加復雜，謂詞的選取和精化過程的開銷也隨之增大，等價類中測試用例之間可約簡的程度也會同時降低，故會生成較多的測試用例。

在程序執行時間上，本文方法在系統模型狀態約簡階段和測試用例生成階段的時間復雜度均為O( k2)，故本文方法的總時間復雜度為O( k2)，前文提到貪心算法、HGS算法和GRE算法這3種典型的啟發式方法的時間復雜度分別為O( mn·min(m, n))、O( m( m+n) k)和O(min(m, n)( m+n2k))，相比之下本文算法有更低的時間復雜度。文獻[13]指出在精確性方面，現有的幾種啟發式方法已被證實任何一種算法都不比其他算法優越，故本文選擇時間復雜度相對較低且易于實施的貪心算法與本文方法進行對比。在測試對象選取上，選擇規模最大的cdaudio程序和規模較小的ping程序。由于前文提到的3種啟發式算法的時間復雜度均為最壞情況下復雜度，故在模擬實驗過程中，該3種啟發式算法的時間開銷比本文方法的略大，通過圖4可以看出，程序規模越大，本文算法在時間開銷上提高的效果越明顯。

在實驗過程中，BLAST所生成的抽象狀態模型本質上是一個有限狀態自動機（FSA），由于FSA無法描述帶有遞歸調用的程序，故在實驗前對程序中含有遞歸調用的部分進行預處理，使之不反映到程序的控制流圖中。在測試用例生成過程中，謂詞抽象自動驗證工具可以根據反例的抽象精化功能，不斷對初始謂詞集合進行完善，同時還可以驗證原始模型不能滿足的性質，以利于對程序所具有的性質的研究。

表1 實驗結果

圖4 算法的時間開銷對比

6 結束語

測試用例的質量和數量決定測試的成本和有效性，但大規模軟件系統往往存在狀態空間爆炸的問題，故難以生成精簡、高效的測試用例集，從而影響對軟件系統所具有性質的驗證。謂詞抽象技術可以有效地減少系統的狀態遷移的數量，以此作為測試用例集約簡生成的基礎。本文提出一種基于謂詞抽象的測試用例約簡生成算法，以系統的狀態遷移關系作為研究目標，通過謂詞集合將原始系統的初始狀態進行等價類劃分，并使用謂詞抽象自動驗證工具的反例引導功能，生成滿足給定性質的測試用例。實驗數據表明，相對于其他幾種典型的測試用例約簡方法，本文的方法可以在較短時間內生成數量較少的測試用例集。

然而本文方法還存在改進的空間，例如對于程序中存在的遞歸調用語句，本文的方法還不能處理，這將限制其使用范圍，將來的工作中，可以考慮使用支持遞歸調用的謂詞抽象驗證工具來改進本文中的方法；另外，對于具有可信特征屬性需求的系統，根據文獻[14]的觀點：可信≈可靠+安全，可以對謂詞的屬性表示方法進行擴展，使本文的方法在具有可靠、安全等非功能特征屬性的系統中也能夠生成約簡的測試用例。

[1] HARROLD M J, GUPTA R, SOFFA M L. A methodology for controlling the size of a test suite[J]. ACM Transactions of Software Engineering and Methodology, 1993, 2(3):270-285.

[2] 屈婉霞, 李暾, 郭陽等. 謂詞抽象技術研究[J]. 軟件學報, 2008,19(1): 27-38.QU W X, LI T, GUO Y, et al. Advances in predicate abstraction[J].Journal of Software, 2008, 19(1): 27-38.

[3] HONG H S, CHA S D, LEE I, et al. Data flow testing as model checking[A]. Proceedings of the 25th International Conference on Software Engineering[C]. Portland, 2003, 232-243.

[4] CHVATAL V. A greedy heuristic for the set-covering problem[J].Mathematics of Operations Research, 1979, 4(3): 233-235.

[5] CHEN T Y, LAU M F. On the completeness of a test suite reduction strategy[J]. The Computer Journal, 1999, 42(5): 430-440.

[6] LEE J G, CHUNG C G. An optimal representative set selection method[J]. Information and Software Technology, 2000, 42(21):17-25.

[7] 章曉芳, 徐寶文, 聶長海等. 一種基于測試需求約簡的測試用例集優化方法[J]. 軟件學報, 2007, 18(4): 821-831.ZHANG X F, XU B W, NIE C H, et al. An approach for optimizing test suite based on testing requirement reduction[J]. Journal of Software, 2007, 18(4): 821-831.

[8] 程亮, 張陽, 馮登國. 一種基于安全狀態轉移的簡并測試集生成方法[J]. 軟件學報，2010，21(3): 539-547.CHENG L, ZHANG Y, FENG D G. Approach of degenerate test set generation based on secure state transition[J]. Journal of Software,2010, 21(3): 539-547.

[9] 徐明迪, 張煥國, 嚴飛. 基于標記變遷系統的可信計算平臺信任鏈測試[J]. 計算機學報, 2009, 32(4): 635-645.XU M D, ZHANG H G, YAN F. Testing on trust chain of trusted computing platform based on labeled transition system[J]. Chinese Journal of Computers, 2009, 32(4): 635-645.

[10] SUSANNE G, HASSEN S. Construction of abstract state graphs with PVS[A]. Proceedings of the 9th International Conference on Computer Aided Verification[C]. Berlin, 1997. 72-83.

[11] HENZINGER T A, JHALA R, MAJUMDAR R. Lazy abstraction[A].ACM Symposium on Principles of Programming Language[C]. Oregon, 2002. 58-70.

[12] DETLEFS D, NELSON G, SAXE J B. Simplify: a theorem prover for program checking[J]. Journal of the ACM, 2005, 52(3): 365-473.

[13] CHEN T Y, LAU M F. A simulation study on some heuristics for test suite reduction[J]. Information and Software Technology, 1998,40(13): 777-787.

[14] 沈昌祥，張煥國，馮登國等. 信息安全綜述[J]. 中國科學E輯, 2007，37(2): 129-150.SHEN C X, ZHANG H G, FENG D G, et al. Survey of information security[J]. Science in China, Series E, Information Sciences, 2007,37(2): 129-150.