約束覆蓋導向的Web服務測試數據生成

程 浩，周 輝，錢 巨

(南京航空航天大學 計算機科學與技術學院，南京 211106)E-mail：jqian@nuaa.edu.cn

1 引 言

Web服務是一種通過網絡支持可互操作的端到端交互的軟件系統(1)http://www.w3.org/TR/ws-gloss.Web服務因其所具有的高通用性、可互操作性與可重用性而受到廣泛關注.與其他軟件系統不同，Web服務使用了基于XML的WSDL標準文檔來描述服務接口，包括服務功能、輸入和輸出，對外隱藏了復雜業務邏輯的實現.

Web服務與其他軟件系統一樣，也存在質量問題，而且由于Web服務廣泛用于各種應用，尤其是電子商務應用，問題可能會更嚴重.為此，研究人員為Web服務的測試技術付出了很多努力[1]，在測試數據生成[2，3]、單元測試[4，5]、測試預言[6]、故障注入技術[7]、回歸測試[8]、安全測試[9]等方面的研究也取得了很多重要成果，但是挑戰依然存在.

Web服務測試的挑戰之一是生成高覆蓋率的測試數據.人們[1]提出了多種測試數據生成方法，包括基于 XML Schema、基于模型、基于規約等方法，其中，基于 XML Schema 的方法根據 WSDL 文檔提供的數據類型信息生成測試數據，基于模型的方法通過構建服務內部的行為模型(如自動機)來生成測試數據[10]，基于規約的方法一般根據 Web 服務輸入和輸出的前置與后置條件來生成測試數據[11].相較而言，基于 XML Schema 的方法快而簡單，但只是根據粗粒度的數據類型信息生成數據，因此無法確保能夠生成有意義的代表性測試數據.基于模型的方法主要適用于 BPEL 組合服務，對于原子服務來說該方法顯得過于復雜.與上述兩種方法相比，基于規約的測試數據生成方法不僅能夠生成更合理的服務輸入，而且在為原子服務生成測試數據時通常要比基于模型的方法更高效.

對于原子服務，文獻[12]提出了一種基于規約的Web服務測試數據生成方法，先用簡單的取值范圍約束(如(a≥0∧a≤10)∧(b≥0∧b≤10))來指定服務的輸入條件，再基于區間劃分技術生成測試數據，測試數據是通過選取每個輸入參數的數據分區中的值組合得到的，但該方法并不支持不同服務輸入參數之間的復雜約束，如a+b

在更廣泛的測試數據生成研究領域中[15,16]，還有一些根據規約約束生成測試數據的黑盒方法，但大多數只關注如何求解約束，并未解決如何操縱約束以生成高覆蓋率測試數據的問題[17]，而且很少有研究方法能夠定義明確的規約約束級測試覆蓋準則，并利用這些準則指導約束求解以生成測試數據.

考慮到上述問題，本文提出了一種基于規約約束的測試數據生成方法，用一階邏輯公式定義服務輸入和輸出的規約約束，能夠根據給定的規約約束生成高覆蓋的測試數據.本方法的重點是測試原子服務，并支持復雜的一階邏輯約束，如(3*a+12)*2<100，以及描述變量間關聯關系的約束，如x+y>z.本文使用Z3 SMT約束求解器生成測試數據，而且為了生成高覆蓋率的測試數據，引入幾種規約約束級覆蓋準則，并提出生成滿足這些準則的測試數據的新算法.實驗通過測試兩個目標服務得到的結果表明，使用新的測試覆蓋準則與相應的測試數據生成算法，可以實現更高的代碼覆蓋率，因此本文提出的方法能夠提高Web服務測試數據的質量.

2 背 景

2.1 Web服務

一個Web服務包含服務實現和服務接口描述，后者通常是由 WSDL 文檔表達.WSDL 文檔內容由抽象類型定義和部署描述兩部分組成.抽象類型定義包括 types、message、portType 等 XML 元素，其中 types 元素描述了該服務中使用的數據類型，可以是簡單數據類型如整型、字符串等，也可以是類似于 C 語言結構體的復雜類型；message 元素描述了服務的輸入和輸出；portType 元素定義了服務支持的操作，操作就像是面向對象語言中類的一個方法.部署描述定義了服務的 URL 和調用服務的協議.這些元素中，types 元素是測試數據生成的關鍵.

圖1是描述Web服務Sum的WSDL文檔，Sum服務有一個sum操作，由部分可知該服務接受三個 int 類型的參數a，b，c，用戶可以通過URL地址調用這個服務，該服務的實現可以用任何語言，但對調用者來說是透明的，而WSDL文檔是用戶可見的.

2.2 基于規約的 Web 服務測試

在基于規約的原子Web服務測試中，每個測試目標由一個三元組表示：

F=，

其中S表示待測的原子Web服務，O是服務S中可被調用的操作，C是由服務S中若干前置條件和后置條件組成的約束系統.前置條件定義了服務輸入應滿足的約束，用于生成Web服務的測試數據，后置條件則定義了服務輸出應滿足的約束，用于檢查測試數據的執行結果.

圖1 WSDL文檔示例
Fig.1 An example WSDL document

2.3 基于 SMT 約束求解器的測試數據生成

為了表達Web服務中輸入和輸出參數之間的關聯關系，本文擬采用一階邏輯公式定義約束，并基于SMT(Satisfiability Modulo Theories，可滿足性模理論)約束求解器[18]生成測試數據.SMT 約束求解器用于查找滿足一階邏輯公式的一組數據，被廣泛用于軟件驗證、測試用例生成等方面.

Z3是微軟發布的一款 SMT 約束求解器[19]，支持各種復雜的理論公式，包括算術表達式、布爾表達式、邏輯表達式等.本文將基于Z3約束求解器生成 Web 服務測試數據.

但是直接使用Z3求解約束得到的測試數據無法保證能夠覆蓋所有的輸入方案，例如，對于以下約束：

a>20∨b<10∨a>b，

使用Z3求解可以得到一個有效的測試數據(a=15，b=12)，該數據只覆蓋了條件子句a>b，未覆蓋a>20和b<10，這種低覆蓋率的測試數據會影響Web服務故障的發現.

3 基于Z3的測試數據生成方法概述

為了解決以上問題，本文提出了一種基于一階邏輯公式規約和Z3約束求解器的高覆蓋率測試數據生成方法，如圖2所示.

圖2 測試數據生成過程Fig.2 Test data generation process

方法的輸入包括待測Web服務的WSDL文檔、服務對應的前置條件約束以及選定的覆蓋準則，方法的輸出是一個滿足輸入覆蓋準則的測試集.測試數據生成的過程包括兩個主要步驟：1)根據覆蓋準則進行約束轉換；2)基于Z3 SMT約束求解器的測試數據生成.生成的測試數據將被封裝于SOAP包中用于 Web 服務測試.表1給出了測試數據生成的一個實例，其中最后一列的測試數據是根據第一列中給定的前置條件生成的.本文主要關注整數類型的變量.

表1 測試數據生成示例Table 1 An example for test data generation

3.1 Web 服務規約語言

Web服務的測試規約由前置條件和后置條件給定，它們都是用一階邏輯公式表達的約束，而且是 SMT 求解器可求解的.與傳統范圍約束(如a<10)只能限定單個變量不同，一階邏輯公式約束能夠定義不同變量之間的關聯關系，例如，a=b或a+b<10 等描述的復雜關系.

規約語言的語法如圖3所示，其中 Variable，Value分別表示約束變量與常數值，expr，bexpr 分別是算術表達式和布爾表達式，constraint 表示約束中的邏輯公式.

圖3 規約語法Fig.3 Grammar of the specification language

規約語法中的約束變量對應于服務操作的輸入或輸出參數，例如，對于圖1中的 Sum 服務，參數a可以表示為：

value(svc/sum/a)，

其中，svc是給定服務的宏定義，svc/sum表示Sum服務支持的操作sum.假定Sum服務的輸入參數必須滿足都相等或者都不相等，對應的規約如圖4所示.規約可以保存在獨立的文件中，也可以集成到XML文檔中.規約提供了更多服務操作的輸入空間信息，通過全面探索輸入空間可以獲得更高覆蓋率的測試數據.

圖4 規約示例Fig.4 An example specification

3.2 WSDL 描述中的限定

目前 WSDL 規范支持一種限定(restriction)機制，以限制服務輸入和輸出的取值，常用的限定類型包括范圍限定和枚舉限定.范圍限定用于限制變量的最大或最小值，圖5(a) 表示參數a的取值范圍是[0，10].枚舉限定給出了變量的有效取值集合，圖5(b) 限定參數b只能取0或1.

(a)范圍限定 (b)枚舉限定

除上述兩種限定之外，還有其他更為復雜的限定在本文中沒有用到.為了生成合理的測試數據，WSDL 描述中的這些限定將被轉換成邏輯約束，并加到約束系統中.結合圖4和圖5可得，Sum 服務中 sum 操作完整的前置條件如下：

Csum=(a≥0∧a≤10)∧(b=0∨b=1)∧

((a≠b∧b≠c)∨(a=b∧b=c))，

本文將使用該約束生成測試數據.

4 基于規約約束的測試覆蓋準則

為了對給定的Web服務生成充足的測試數據，本文定義了幾種規約約束級測試覆蓋準則，涵蓋了更多基于規約約束的情形，基于這些準則進行測試可以為指定服務測試更多的輸入方案.規約約束級測試覆蓋準則包括判定覆蓋、條件覆蓋、判定條件覆蓋、范式子句覆蓋，這些準則借鑒了白盒測試中代碼級覆蓋的部分概念.

4.1 判定覆蓋

在白盒測試中，判定覆蓋要求測試用例能夠覆蓋每個判定中真或假的結果.在基于規約約束的測試中，判定覆蓋則要求測試數據不僅要滿足規約約束(有效數據)，還要滿足約束的否定形式(無效數據).

定義1.(判定覆蓋) 對于給定前置條件C的服務，如果測試集T滿足以下條件：

?t∈T，eval(C，t)=true∧?t′∈T，eval(C，t′)=false，

就稱測試集T滿足判定覆蓋，其中eval(C，t) 用于判斷測試數據t是否滿足約束C.

對于3.2節給出的規約約束Csum，測試集Tdc(a，b，c)={(1，1，1)，(20，1，1)} 覆蓋了有效數據和無效數據，因此該測試集滿足判定覆蓋.

4.2 條件覆蓋

判定覆蓋無法保證給定的測試集能夠覆蓋所有產生有效測試數據或者無效數據的不同情形.例如，Tdc沒有覆蓋b=0的情況.一種提高覆蓋率的途徑是要求測試集能覆蓋每個基本條件的不同結果.在白盒測試中，這種覆蓋叫做條件覆蓋，本文將其引入到規約約束級覆蓋準則中.在基于規約約束的測試中，條件覆蓋要求測試數據不僅要滿足服務參數前置條件中的原子條件，還要滿足各原子條件的否定形式.

定義2.(條件覆蓋) 對于給定前置條件C的服務，如果測試集T滿足以下條件：

?e∈BExpr(C){?t∈T，eval(e，t)=true
∧?t′∈T，eval(e，t′)=false}，

就稱測試集T滿足判定覆蓋，其中BExpr(C)是前置條件C中原子條件的集合.

對于3.2節給出的規約約束Csum，測試集Tcc(a，b，c)={(1，1，1)，(-1，0，-1)，(20，0，20)} 能保證覆蓋所有的原子條件及各自的否定形式，因此該測試集滿足條件覆蓋.

4.3 判定條件覆蓋

對于(a>b∨c>d)類似的約束，覆蓋每個原子條件的不同結果并不能保證覆蓋整個約束真或假的結果.為此，本文定義了規約約束級的判定條件覆蓋準則.在基于規約約束的測試中，判定條件覆蓋要求為給定前置條件的Web服務生成的測試數據不僅要滿足判定覆蓋，還要滿足條件覆蓋.

定義3.(判定條件覆蓋) 對于給定前置條件C的服務，如果測試集T滿足以下條件：

?t∈T，eval(C，t)=true∧?t′∈T，eval(C，t′)=false
∧?e∈BExpr(C){?t∈T，eval(e，t)=true
∧?t′∈T，eval(e，t′)=false}，

就稱測試集T滿足判定條件覆蓋.

對于3.2節給出的規約約束Csum，4.2節中的測試集Tcc符合上述定義，因此該測試集滿足判定條件覆蓋.

4.4 范式子句覆蓋

對于規約約束，當測試數據有效時析取范式(DNF)會有不同的情況，當測試數據無效時合取范式的否定則會有不同的情況.這些情況常對應于 Web 服務的不同行為，因此應更好地被測試集覆蓋.然而條件覆蓋和判定條件覆蓋都不能保證這些情況都能被覆蓋.例如，測試集Tcc雖然覆蓋了b=0和b=1的情況，但是并未覆蓋b的取值不在集合{0，1}中的情況.

為此，本文介紹一種范式子句覆蓋準則，要求測試數據不僅要滿足前置條件中析取范式的每個子句，還要滿足合取范式中每個子句的否定.這樣一來，產生有效數據或無效數據的不同情形都能被覆蓋到.

定義4.(范式子句覆蓋)對于給定前置條件C的服務，如果測試集T滿足以下條件：

?f∈DNF(C)，?t∈T，eval(f，t)=true
∧?f∈CNF(C)，?t′∈T，eval(f，t′)=false，

就稱測試集T滿足范式子句覆蓋，其中DNF(C)、CNF(C) 分別是前置條件C中析取范式子句、合取范式子句的集合.

對于3.2節給出的規約約束Csum，析取范式子句有：

(a≥0∧a≤10)∧(b=0)∧(a≠b∧b≠c)，

(a≥0∧a≤10)∧(b=0)∧(a=b∧b=c)，

(a≥0∧a≤10)∧(b=1)∧(a≠b∧b≠c)，

(a≥0∧a≤10)∧(b=1)∧(a=b∧b=c)，

合取范式包括：

a≥0，a≤10，(b=0∨b=1)，(a≠b∨a=b)，

(b≠c∨a=b)，(a≠b∨b=c)，(b≠c∨b=c).

根據這些子句生成的測試集Tnfcc(a，b，c)={(1，0，2)，(0，0，0)，(0，1，2)，(1，1，1)，((1，0，2)，(11，0，2)，(1，2，2)，(1，1，0)，(0，1，1)} 滿足范式子句覆蓋.

5 測試數據生成算法

設Z3是根據給定約束生成有效隨機數據的函數，本節將基于Z3函數介紹滿足不同測試覆蓋準則的測試數據生成算法.

5.1 滿足判定覆蓋的測試數據生成算法

對于給定前置條件C的服務，通過將Z3函數作用于條件C及其否定形式C，可以生成滿足判定覆蓋的測試集T：

T={Z3(C)，Z3(C)}.

對于3.2節給出的規約，滿足判定覆蓋的測試集可通過將Csum代入上式得到：

Tdc(a，b，c)={(1，1，1)，(20，1，1)}.

5.2 滿足條件覆蓋的測試數據生成算法

對于給定前置條件C的服務，其中C的原子條件集合為BExpr(C)，若要生成滿足條件覆蓋的測試集，則要求數據集同時滿足BExpr(C)中的每個條件e及其否定形式e.由于滿足條件e的測試數據也可能滿足其他條件，因此根據每個條件直接生成對應的數據會帶來冗余，為此，本文使用算法1所示的工作隊列算法來生成整個測試集.

算法1.滿足條件覆蓋的測試數據生成算法

Input：C：規約約束

Output：T：測試集

Begin

E=BExpr(C)∪ {e|e∈BExpr(C)};

whileE≠?do

removeeifromE;

t：=Z3(ei∧C);

ift≠ nullthenT：=T∪ {t};

else

t：=Z3(ei∧C);

ift≠ nullthenT：=T∪ {t}；end

end

foreachek∈Edo

ifeval(ek，t)==truethen

E：=E-{ek}；

end

end

end

returnT;

End

算法首先創建包含所有需要覆蓋的條件的工作隊列E，然后根據E中的每個條件ei使用Z3生成對應的服務輸入t.為了生成合理的完整輸入，需要先將ei和前置條件C(或其否定形式C)進行邏輯與操作，再用Z3 求解得到輸入數據t，此時從工作隊列E中刪除ei，而且t滿足的其他條件也要刪除.當工作隊列E為空時算法終止.

對于3.2節給出的規約約束Csum，首先創建工作隊列E={e1=(a≥0)，e2=(a≤10)，e3=(b=0)，e4=(b=1)，e5=(a≠b)，e6=(b≠c)，e7=(a=b)，e8=(b=c)，e1，e2，e3，e4，e5，e6，e7，e8}，然后根據條件e1使用Z32http://axis.apache.org/axis2/java/core

生成服務輸入t1=(1，1，1)，t1也滿足條件e2，e4，e7，e8，e3，e5以及e6，因此將這些條件從E中刪除，得到E={e3，e5，e6，e1，e2，e4，e7，e8}.接下來根據條件e3使用Z3生成另一個服務輸入t2=(-1，0，-1)，t2也滿足條件e5，e6，e1，e4，e7以及e8，將這些條件從工作隊列中刪除后得到E={e2}.最后使用Z3求解到服務輸入(20，0，20)，算法終止.最終的測試數據集合為Tcc(a，b，c)={(1，1，1)，(-1，0，-1)，(20，0，20)}.

5.3 滿足判定條件覆蓋的測試數據生成算法

對于給定前置條件C的服務，要生成滿足判定條件覆蓋的測試集，可以先生成滿足條件覆蓋的測試數據集，再向其中加入必要的測試數據以確保滿足判定覆蓋.詳細的測試數據生成算法如算法2所示.算法首先調用CC(C)生成滿足BExpr(C) 中的每個條件e及其否定形式e的測試數據集，然后判斷該數據集是否同時滿足條件C及其否定形式C，若不滿足條件C，則根據條件C使用Z3生成服務輸入；若不滿足條件C，則根據條件C使用Z3生成對應的服務輸入.

算法2.滿足判定條件覆蓋的測試數據生成算法

Input：C：規約約束

Output：T：測試集

Begin

T：=CC(C);

B：=?；

foreacht∈TdoB：=B∪ {eval(C，t) };end

iftrue?BthenT：=T∪Z3(C);

elseiffalse?BthenT：=T∪Z3(C);

end

returnT;

End

對于3.2節給出的規約約束Csum，算法首先使用CC(C)得到滿足條件覆蓋的測試集Tdcc={(1，1，1)，(-1，0，-1)，(20，0，20)}，Tdcc同時滿足條件C及其否定形式C，因此Tdcc滿足判定條件覆蓋，無需生成額外的輸入以滿足判定覆蓋.

5.4 滿足范式子句覆蓋的測試數據生成算法

對于給定前置條件C的服務，其中C的析取范式子句集合、合取范式子句集合分別為DNF(C)、CNF(C)，為了生成滿足范式子句覆蓋的測試集，需要生成包括滿足DNF(C)中每個子句的數據，以及不滿足CNF(C)中每個子句的數據，具體過程如算法3所示.

算法3.滿足范式子句覆蓋的測試數據生成算法

Input：C：規約約束

Output：T：測試集

Begin

F=DNF(C)∪{e|e∈CNF(C)};

foreache∈Fdo

t：=Z3(e);

T：=T∪{t};

end

returnT;

End

對于3.2節給出的規約約束Csum，算法首先得到需要覆蓋的9個范式子句，由4.4節中給出，然后使用Z3 為每個子句生成相應的服務輸入，最終的數據集為4.4節中的Tnfcc.

6 實 驗

為了驗證本方法的有效性，我們實現了該方法并在兩個 Web 服務上對其進行測試，以回答以下的研究問題：

問題1.本文提出的測試覆蓋準則在缺陷檢測方面的表現如何？

實驗并未為服務注入故障，主要通過檢查這些測試覆蓋準則是否可以帶來更高的代碼級覆蓋率來回答這個問題.

問題2.本文中的測試數據生成算法能否用更少的測試數據來滿足文中提出的測試覆蓋準則？

問題3.測試數據生成算法的效率如何？

6.1 實驗設置

實驗用本文提出的方法分別測試了兩個典型的Web服務：Triangle與MiddleNumber[12，20，21]，這些服務的變體廣泛用于軟件測試研究中.Triangle服務根據輸入三角形的三條邊長a，b，c判斷該三角形是一般三角形、等腰三角形還是等邊三角形，MiddleNumber服務根據輸入的三個數i，j，k判斷k是否為介于i和j之間的中間數字.實驗用Java實現這些服務，并將它們部署在Axis2容器2中，測試數據生成算法也用Java實現，實驗用Java版的Z3進行約束求解.

為了生成測試數據，實驗為兩個服務定義了前置條件.實驗對本文提出的測試數據生成算法與現有方法進行代碼覆蓋率和效率的比較，以說明本方法的有效性.

Triangle服務的前置條件如下：

CT=C1∧C2，

C1=(a>0)∧(b>0)∧(c>0)∧(a<100)

∧(b<100)∧(c<100)∧(a+b>c)

∧(b+c>a)∧(a+c>b)，

C2=((a=b∧a≠c)∨(b=c∧b≠a)∨(a=c∧a≠b))

∨(a=b∧b=c)∨(a≠b∧a≠c∧c≠b)).

其中，條件C1對邊長的范圍做出限制以形成一個有效的三角形，條件C2列舉了所有可能的三角形類型的條件，以覆蓋更多的輸入情況.

MiddleNumber服務的前置條件如下：

CM=(i>0)∧(j>0)∧(k>0)

∧(i<100)∧(j<100)∧(k<100)

∧((k>i)∧(kj)).

該條件對輸入參數的值進行范圍限制，并要求k介于i和j之間.

表2列出了Triangle和MiddleNumber服務的前置條件約束，其中文獻[12]提出的測試生成方法(本文稱其為MATDG)并不支持變量之間的關聯約束，表中的約束是簡化后得到的.

6.2 實驗結果

問題1.本文提出的測試覆蓋準則在缺陷檢測方面的表現如何？

實驗通過比較MATDG[12]、隨機方法以及本文所提方法的代碼級語句覆蓋率和分支覆蓋率來回答這個問題：代碼覆蓋率越高，缺陷檢測能力越好.

實驗分別對Triangle和MiddleNumber服務進行測試，實驗結果如表3所列，其中SC%、BC%分別表示語句覆蓋率和分支覆蓋率，CN是不同方法生成的測試數據數量，Avg是每種方法對應統計項的均值.

對于MATDG方法，實驗在兩種典型配置下生成測試數據<0，1>與<1，1>(配置表示分別為參數的每個無效等價類和有效等價類生成m和n個輸入，然后將它們組合成不同的測試數據)；對于隨機方法，實驗分別生成5個、10個測試數據以評估隨機方法的有效性；對于本文基于規約的方法，實驗分別生成滿足第4節中四種覆蓋準則的測試數據.表3為每個服務分別統計了幾種代碼的覆蓋率，包括用于拒絕非法輸入的防御代碼、用于正常計算的代碼以及總代碼.根據表3的結果，圖6中(a)和(b)分別用條形圖對三種方法的語句覆蓋率和分支覆蓋率進行更直觀地比較.顯然，本文基于規約約束的方法同時具有最高的語句覆蓋率和分支覆蓋率.

表2 Web服務的規約約束Table 2 Specification constraints of Web services

表3 生成測試數據的語句覆蓋率(SC)和分支覆蓋率(BC)Table 3 Generated test data and their statement coverage(SC) and branch coverage(BC) rates

圖6 比較三種方法的語句覆蓋率和分支覆蓋率Fig.6 Comparison of the three evaluated approaches in source code level statement and branch coverages

然而，有些語句和分支仍未覆蓋到，這是因為使用有限數量的測試用例很難覆蓋所有的條件組合，滿足范式子句覆蓋的測試用例覆蓋了最多的分支和語句，尤其是正常計算代碼的覆蓋方面.

問題2.本文中的測試數據生成算法能否用更少的測試數據來滿足文中提出的測試覆蓋準則？

實驗通過比較達到相同規約約束級覆蓋率時隨機方法生成的測試用例數量與本文所提方法生成的測試用例數量來回答這個問題：數量越少，效果越好.

表4列出了滿足四種規約約束級覆蓋準則所需的測試用例數量，可以看出，基于規約約束的方法只要使用少許幾個測試用例就能滿足規約約束級覆蓋準則，而隨機方法需要數百個用例才能達到相同的覆蓋率，因此基于 Z3 的算法在給定覆蓋準則下可以更為有效地生成低冗余的測試用例.

問題3.測試數據生成算法的效率如何？

圖7 生成測試數據的時間Fig.7 Time spent on test data generation

實驗通過收集生成分別滿足四個規約約束級覆蓋標準的測試數據所花費的時間來說明測試數據生成算法的效率.圖7給出了為Triangle 服務和 MiddleNumber 服務生成測試數據時所花費的時間，可以看出，生成滿足判定覆蓋(DC)的測試數據所花時間最少，生成滿足范式子句覆蓋(NFCC)的測試數據所花時間稍多一點，而生成滿足條件覆蓋(CC)和判定條件覆蓋(DCC)的測試數據需要花費更多的時間.結合表3中的語句和分支覆蓋率可以得到以下結論：使用范式子句覆蓋準則生成的測試數據更有效，而且效率更高.

表4 達到不同規約約束級覆蓋率時的測試用例數量Table 4 Test cases needed to achieve coverages at the different level of specification constraints

7 結束語

本文提出了一種基于規約約束的 Web 服務測試數據生成方法，該方法中使用的規約約束系統不僅支持簡單的服務輸入取值范圍約束，而且還支持服務輸入參數之間的復雜關聯約束.本文還提出了四種規約約束級覆蓋準則——判定覆蓋、條件覆蓋、判定條件覆蓋以及范式子句覆蓋.利用這些覆蓋準則，可以通過 Z3 SMT 求解器產生高覆蓋率的測試數據，從而更好地揭示服務中的缺陷.本文的研究仍然存在一些不足，首先，實驗論證還有待在更大規模、更復雜 Web 服務上做進一步加強，另外，盡管本文的方法已經能夠達到較高測試覆蓋率，但仍有進一步提升的空間.為此，未來將開展更多實驗研究，為方法的應用提供更多參考.同時，計劃不斷研究新的覆蓋準則，如結構化測試中的修正條件判定覆蓋準則(MC/DC)[22]等，以完善所提出的方法.