郭曦，張煥國,2

(1. 武漢大學(xué) 計(jì)算機(jī)學(xué)院，湖北 武漢 430072；2. 武漢大學(xué) 空天信息安全與可信計(jì)算教育部重點(diǎn)實(shí)驗(yàn)室，湖北 武漢 430072)

1 引言

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

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

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

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

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

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

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

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

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

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

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

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

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

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

為了更好地表示軟件系統(tǒng)的狀態(tài)以及狀態(tài)間的遷移關(guān)系，通過謂詞抽象技術(shù)，使用謂詞表示軟件系統(tǒng)的狀態(tài)變遷，可以有效地對(duì)大規(guī)模軟件系統(tǒng)的狀態(tài)進(jìn)行約簡。謂詞抽象使用一組有限數(shù)量的謂詞把系統(tǒng)表示為有限狀態(tài)機(jī)模型，該模型就是對(duì)原始系統(tǒng)的一種抽象，它較原始系統(tǒng)有更小的狀態(tài)集合，其中每一種狀態(tài)屬于一個(gè)等價(jià)類，每個(gè)等價(jià)類里面包含若干個(gè)滿足謂詞劃分的原始狀態(tài)。本節(jié)還證明了一個(gè)基于原始模型系統(tǒng)狀態(tài)空間的問題：經(jīng)過等價(jià)類劃分后得到若干個(gè)子問題，其中每個(gè)等價(jià)類對(duì)應(yīng)一個(gè)子問題，首先對(duì)子問題進(jìn)行求解，再將各子問題的解組合起來就得到原問題的解，該方法可以用來指導(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上定義一個(gè)等價(jià)關(guān)系，該等價(jià)關(guān)系把原始模型的初始狀態(tài)集合劃分成若干個(gè)等價(jià)類，每個(gè)等價(jià)類包含一個(gè)或多個(gè)狀態(tài)，2個(gè)狀態(tài)等價(jià)當(dāng)且僅當(dāng)它們屬于同一個(gè)等價(jià)類。對(duì)于一組謂詞Φ=(φ1,φ2,…,φn)，和一組與之對(duì)應(yīng)的布爾變量B=(B1, B2,…,Bn)，使用謂詞公式φ來表示原始模型的狀態(tài)C，并使用變量B1, B2,…,Bn上的一組正交布爾表達(dá)式來表示對(duì)應(yīng)的抽象模型的狀態(tài)集合A。抽象狀態(tài)表示為A( B1, B2,…,Bn)，其初始狀態(tài)集合記為IA，每個(gè)抽象狀態(tài)與一個(gè)等價(jià)類相對(duì)應(yīng)。為了表示模型的原始狀態(tài)和抽象狀態(tài)之間的關(guān)系，給出如下定義。

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

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

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

3.2 基于等價(jià)類劃分的問題求解

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

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

1) Ci是C的一個(gè)子集；

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

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

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

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

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

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

4 測試用例約簡生成方法

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

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

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

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

定義5 對(duì)于一個(gè)原始模型的狀態(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á)情況，并能夠指導(dǎo)系統(tǒng)狀態(tài)的等價(jià)關(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)，φ對(duì)應(yīng)的原始狀態(tài)遷移關(guān)系記為，其中Rφ?RC，Rφ是原始狀態(tài)φ對(duì)應(yīng)的原始模型狀態(tài)遷移關(guān)系，則與Tj關(guān)聯(lián)的抽象模型狀態(tài)遷移關(guān)系通過如下表達(dá)式確定[10]：

其中，pj是Tj的進(jìn)行語義操作的決定條件，即當(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。

輸出：相對(duì)于謂詞集合Φ的抽象模型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中取出一個(gè)抽象狀態(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)遷移集合，由于每個(gè)抽象狀態(tài)對(duì)應(yīng)一個(gè)等價(jià)類，故以每一個(gè)等價(jià)類中的狀態(tài)遷移集合為研究對(duì)象，通過謂詞抽象自動(dòng)驗(yàn)證工具對(duì)原始模型所具有的性質(zhì)進(jìn)行驗(yàn)證，若不滿足該性質(zhì)，工具可以自動(dòng)返回不滿足該性質(zhì)的程序執(zhí)行路徑，并以此生成針對(duì)每個(gè)等價(jià)類的測試用例集。依據(jù)定理1，把抽象狀態(tài)中每個(gè)等價(jià)類的測試用例組合起來，就可以得到原始模型的約簡測試用例。

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

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

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

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

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

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

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

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

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

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

算法2 每個(gè)等價(jià)類的測試用例約簡生成算法。

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

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

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

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

3) while(P不為空)

4) 從P中選擇一條待驗(yàn)證的性質(zhì)p;

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

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

7) foreachpi∈P( pi≠p)do

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

圖1顯示了對(duì)測試用例進(jìn)行約簡過程，其中圖1(a)表示3個(gè)測試用例：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ù)測試用例進(jìn)行測試環(huán)境初始化所帶來的開銷。

圖1 測試用例約簡過程

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

對(duì)于每個(gè)等價(jià)類生成的約簡測試用例集{RT1, RT2,…,RTk}，其中k=|IA|，把RT1, RT2,…,RTk依據(jù)算法1得到的抽象狀態(tài)遷移關(guān)系RA進(jìn)行連接就可以得到對(duì)應(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，對(duì)于RT1→RT2，把RT1中的每條測試用例與RT2中的每條測試用例依據(jù)原始狀態(tài)遷移關(guān)系集合RC進(jìn)行連接，依次拓展到RTk。

圖2表示2個(gè)測試用例的連接過程，設(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 不同等價(jià)類的測試用例連接過程

4.3 狀態(tài)約簡實(shí)例分析

本節(jié)通過一個(gè)實(shí)例，對(duì)基于謂詞抽象方法的原始模型狀態(tài)約簡過程進(jìn)行描述。對(duì)于一個(gè)原始模型，設(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)相對(duì)于謂詞集合Φ的抽象狀態(tài)為

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

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

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

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

5 測試用例約簡生成的仿真實(shí)驗(yàn)

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

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

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

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

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

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

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

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

圖4 算法的時(shí)間開銷對(duì)比

6 結(jié)束語

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

然而本文方法還存在改進(jìn)的空間，例如對(duì)于程序中存在的遞歸調(diào)用語句，本文的方法還不能處理，這將限制其使用范圍，將來的工作中，可以考慮使用支持遞歸調(diào)用的謂詞抽象驗(yàn)證工具來改進(jìn)本文中的方法；另外，對(duì)于具有可信特征屬性需求的系統(tǒng)，根據(jù)文獻(xiàn)[14]的觀點(diǎn)：可信≈可靠+安全，可以對(duì)謂詞的屬性表示方法進(jìn)行擴(kuò)展，使本文的方法在具有可靠、安全等非功能特征屬性的系統(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é)報(bào), 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é)報(bào), 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é)報(bào)，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] 徐明迪, 張煥國, 嚴(yán)飛. 基于標(biāo)記變遷系統(tǒng)的可信計(jì)算平臺(tái)信任鏈測試[J]. 計(jì)算機(jī)學(xué)報(bào), 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.