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

郭曦，張煥國,2

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

1 引言

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

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

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

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

2 相關(guān)工作及存在的問題

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

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

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

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

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

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

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

3 系統(tǒng)模型狀態(tài)約簡與等價類的問題求解

對于一個軟件系統(tǒng)，理想的測試用例集是在滿足測試需求的基礎(chǔ)上，用例的數(shù)量要盡可能少?，F(xiàn)有的二叉判定圖和樹型結(jié)構(gòu)等約簡測試用例的方法，都是以系統(tǒng)所能達到的狀態(tài)作為操作對象。實際上，決定測試用例集規(guī)模的直接因素往往不是系統(tǒng)的狀態(tài)數(shù)量，而是狀態(tài)遷移的數(shù)量。

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

3.1 抽象狀態(tài)的形式化定義

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

定義1 抽象算子α把模型的原始狀態(tài)φ映射到抽象模型對應(yīng)的抽象狀態(tài)：

定義2 精化算子γ將抽象模型對應(yīng)的抽象狀態(tài)映射到模型的原始狀態(tài)：

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

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

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

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

1) Ci是C的一個子集；

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

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

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

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

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

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

4 測試用例約簡生成方法

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

4.1 抽象模型狀態(tài)遷移生成算法

基于謂詞的抽象模型的狀態(tài)取決于所使用的謂詞集合，狀態(tài)遷移關(guān)系的復(fù)雜程度對測試用例的構(gòu)造有直接關(guān)系，故需要生成抽象狀態(tài)的遷移關(guān)系，下面給出系統(tǒng)模型M遷移關(guān)系的定義及其性質(zhì)。

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

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

定義6 直接遷移和間接遷移統(tǒng)稱為遷移關(guān)系。

遷移關(guān)系反映出系統(tǒng)狀態(tài)之間的轉(zhuǎn)換關(guān)系以及狀態(tài)的可達情況，并能夠指導(dǎo)系統(tǒng)狀態(tài)的等價關(guān)系的構(gòu)建。下面給出遷移關(guān)系的性質(zhì)。

性質(zhì)1 遷移關(guān)系具有傳遞性，即如果1c和2c之間、2c和3c之間均存在遷移關(guān)系，則1c和3c之間存在遷移關(guān)系。

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

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

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

算法1 抽象模型的狀態(tài)遷移關(guān)系生成算法。

輸入：謂詞集合Φ、原始模型的初始狀態(tài)集合IC，狀態(tài)遷移關(guān)系集合RC。

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

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

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

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

4) Atran:=null; //初始化狀態(tài)遷移關(guān)系

5) while(Arest不為空)

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

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

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

11) end while

12) returnAtran;

4.2 基于狀態(tài)約簡的測試用例生成算法

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

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

1) 包含關(guān)系：若ti∩tj=ti，則ti包含于tj，記為ti?tj，它表明ti對應(yīng)的狀態(tài)遷移集合包含在tj對應(yīng)的狀態(tài)遷移集合中。

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

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

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

若ti?tj，由于ti對應(yīng)的狀態(tài)遷移集合包含在tj對應(yīng)的狀態(tài)遷移集合之中，故約簡后的結(jié)果是ti。

若ti⊕tj，由于ti和tj之間存在部分重合關(guān)系，將ti和tj對應(yīng)的測試用例重合的部分作為約簡后的結(jié)果，即保留ti∩tj。

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

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

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

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

輸入：經(jīng)形式化描述的待驗證的性質(zhì)集合P。

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

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

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

3) while(P不為空)

4) 從P中選擇一條待驗證的性質(zhì)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;//生成已包含在之前測試用例所覆蓋的狀態(tài)

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

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

圖1 測試用例約簡過程

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

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

圖2表示2個測試用例的連接過程，設(shè)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 狀態(tài)約簡實例分析

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

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

此時，抽象模型對應(yīng)的抽象狀態(tài)集合A為

抽象狀態(tài)所對應(yīng)的遷移關(guān)系集合：

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

圖3 謂詞抽象處理前后系統(tǒng)狀態(tài)的遷移關(guān)系

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

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

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

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

測試對象為kbfiltr、floppy、cdaudio及ping，其中，前3個分別是關(guān)于鍵盤、軟驅(qū)和音頻的設(shè)備驅(qū)動程序，ping是一個網(wǎng)絡(luò)監(jiān)測工具。仿真實驗中待驗證的性質(zhì)為程序的狀態(tài)覆蓋，通過生成約簡的測試用例集以滿足該性質(zhì)。實驗結(jié)果如表1所示，其中T-G、T-HGS、T-GRE分別為對測試對象使用貪心算法、啟發(fā)式算法和GRE算法所生成的測試用例個數(shù)。

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

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

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

表1 實驗結(jié)果

圖4 算法的時間開銷對比

6 結(jié)束語

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

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

[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] 屈婉霞, 李暾, 郭陽等. 謂詞抽象技術(shù)研究[J]. 軟件學(xué)報, 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] 章曉芳, 徐寶文, 聶長海等. 一種基于測試需求約簡的測試用例集優(yōu)化方法[J]. 軟件學(xué)報, 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] 程亮, 張陽, 馮登國. 一種基于安全狀態(tài)轉(zhuǎn)移的簡并測試集生成方法[J]. 軟件學(xué)報，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] 徐明迪, 張煥國, 嚴飛. 基于標記變遷系統(tǒng)的可信計算平臺信任鏈測試[J]. 計算機學(xué)報, 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]. 中國科學(xué)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.