李昌建 錢巨 程浩 周輝

摘要：面向服務(wù)的軟件體系結(jié)構(gòu)近年來不僅在民用領(lǐng)域得到廣泛應(yīng)用，也越來越多地應(yīng)用于軍用裝備軟件系統(tǒng)研制。服務(wù)化軟件的測(cè)試技術(shù)得到了越來越多的關(guān)注。傳統(tǒng)的服務(wù)化軟件測(cè)試工具大多關(guān)注于測(cè)試流程的自動(dòng)化，在測(cè)試用例的自動(dòng)生成等方面，還遠(yuǎn)不夠成熟?，F(xiàn)有測(cè)試技術(shù)和工具尤其難以表達(dá)真實(shí)應(yīng)用中的業(yè)務(wù)邏輯規(guī)則，給生成高質(zhì)量的測(cè)試帶來許多困難。鑒于此，研發(fā)了一款針對(duì)服務(wù)化系統(tǒng)的軟件測(cè)試原型工具。該工具運(yùn)用一階邏輯公式表達(dá)業(yè)務(wù)邏輯約束，基于23 SMT約束求解器生成測(cè)試用例、進(jìn)行故障注入等，使得測(cè)試數(shù)據(jù)的生成更契合待測(cè)軟件業(yè)務(wù)特征，為服務(wù)化軟件的測(cè)試實(shí)踐提供了更有力支持。

關(guān)鍵詞：Web服務(wù);軟件測(cè)試;測(cè)試用例生成;故障注入;SMT

中圖分類號(hào)：TP311

文獻(xiàn)標(biāo)識(shí)碼：A

面向服務(wù)的軟件體系結(jié)構(gòu)近年來不僅在民用領(lǐng)域得到廣泛應(yīng)用，也越來越多地應(yīng)用于軍用裝備軟件系統(tǒng)研制。包括我國(guó)在內(nèi)，許多國(guó)家的C4ISR軍用信息系統(tǒng)中均已開始應(yīng)用Web服務(wù)技術(shù)[1]。Web服務(wù)技術(shù)的廣泛應(yīng)用對(duì)服務(wù)化軟件系統(tǒng)的可靠性、安全性提出了更高要求。作為保障可靠性與安全性的一種重要手段，服務(wù)化軟件的測(cè)試技術(shù)也得到了越來越多的關(guān)注。國(guó)外的SoapUI[2]、ParasoftSOAtest[3]、SoapSnoar[4]等工具，已為Web服務(wù)系統(tǒng)的測(cè)試提供了許多支持。研究者們也廣泛探討了各類Web服務(wù)測(cè)試技術(shù)[5][6]。然而，現(xiàn)有的服務(wù)化軟件測(cè)試工具大多關(guān)注于測(cè)試流程的自動(dòng)化，重在運(yùn)用工具來完成消息報(bào)文的發(fā)送和收集等。在測(cè)試用例的自動(dòng)生成等方面，還遠(yuǎn)不夠成熟?，F(xiàn)有測(cè)試技術(shù)和工具尤其難以表達(dá)真實(shí)應(yīng)用中的業(yè)務(wù)邏輯規(guī)則，給生成高質(zhì)量的測(cè)試帶來許多困難。比如，在服務(wù)單元的測(cè)試用例生成方面，大多數(shù)工具僅能根據(jù)整數(shù)、浮點(diǎn)數(shù)等接口數(shù)據(jù)類型，使用隨機(jī)、邊界值等方式生成測(cè)試數(shù)據(jù)。對(duì)于接口數(shù)據(jù)存在復(fù)雜業(yè)務(wù)邏輯相關(guān)約束條件的情況處理能力較為有限，生成的測(cè)試數(shù)據(jù)不貼近待測(cè)應(yīng)用的業(yè)務(wù)特性，有效性較差。德國(guó)的Heckel等[7]、北京大學(xué)的姜瑛等[8]、清華大學(xué)的白曉穎等[9]、西北工業(yè)大學(xué)侯俊等[10]研究了數(shù)據(jù)存在約束條件情況下的測(cè)試用例生成問題。他們用區(qū)間限制、OWL-S等機(jī)制表達(dá)接口數(shù)據(jù)上存在的約束。其中，盡管OWL-S等機(jī)制具有較強(qiáng)的約束表達(dá)能力，但這些工作在根據(jù)約束生成測(cè)試用例時(shí)，大多只能處理約束施加在單一輸入因素上的情況，對(duì)于形如a

隨著SMT求解[11]等技術(shù)的發(fā)展，約束系統(tǒng)在表達(dá)能力和求解能力等方面得到了長(zhǎng)足進(jìn)步，也涌現(xiàn)了23[12]等一批成熟的約束求解工具，為構(gòu)建新型的基于約束求解的測(cè)試工具提供了契機(jī)。據(jù)此，本文提出了一個(gè)基于約束的服務(wù)化軟件測(cè)試原型工具，該工具使用一階邏輯作為約束的主要表達(dá)方式，利用23 SMT約束求解器來支持復(fù)雜約束條件下的測(cè)試用例生成。除了將約束求解技術(shù)應(yīng)用于Web服務(wù)單元級(jí)的測(cè)試用例生成，工具還將約束求解技術(shù)應(yīng)用于服務(wù)調(diào)用序列的生成、基于符號(hào)執(zhí)行的組合服務(wù)測(cè)試數(shù)據(jù)生成、面向業(yè)務(wù)邏輯的故障注入等方面，拓寬了約束系統(tǒng)在服務(wù)化軟件測(cè)試領(lǐng)域的應(yīng)用范圍。在測(cè)試方法支持的數(shù)據(jù)類型及類型上的運(yùn)算方面，借助23工具強(qiáng)大的約束求解能力，工具不僅能夠支持一般整數(shù)類型上的線性運(yùn)算，還能夠?qū)Ω↑c(diǎn)數(shù)上的測(cè)試數(shù)據(jù)。生成提供一定程度的支持，甚至支持按位運(yùn)算等約束系統(tǒng)中可能出現(xiàn)的復(fù)雜運(yùn)算公式。通過對(duì)字符串進(jìn)行整數(shù)編碼，以及應(yīng)用基于正則表達(dá)式的字符串生成等技術(shù)，拓廣了測(cè)試功能能夠支持的Web服務(wù)類型范圍。

1 系統(tǒng)結(jié)構(gòu)

Web服務(wù)測(cè)試原型工具基本界面如圖1所示。該工具支持Web服務(wù)描述的靜態(tài)檢測(cè)、服務(wù)單元測(cè)試、服務(wù)調(diào)用序列測(cè)試、組合服務(wù)測(cè)試、服務(wù)故障注入測(cè)試、Web服務(wù)性能測(cè)試等核心功能，如圖2所示。其中，工具通過獨(dú)立的約束系統(tǒng)管理模塊，來維護(hù)待測(cè)項(xiàng)目中的各種業(yè)務(wù)邏約束。這些約束依賴于待測(cè)應(yīng)用的功能特性，而非測(cè)試過程中的某一具體活動(dòng)，可廣泛應(yīng)用在服務(wù)單元的測(cè)試用例生成、服務(wù)調(diào)用序列生成、組合服務(wù)測(cè)試用例生成、服務(wù)故障注入等多個(gè)方面。

為保證靈活性，測(cè)試工具采用了如圖3所示的物理結(jié)構(gòu)。整個(gè)系統(tǒng)由測(cè)試用例設(shè)計(jì)器TestDe-signer、測(cè)試任務(wù)執(zhí)行器ServiceExecutor、服務(wù)部署容器SvcHost、以及代理轉(zhuǎn)發(fā)網(wǎng)關(guān)RedirectProxy四大基本模塊構(gòu)成。

測(cè)試用例設(shè)計(jì)器TestDesigner負(fù)責(zé)測(cè)試用例的設(shè)計(jì)、測(cè)試結(jié)果的收集等任務(wù)，提供一個(gè)用戶界面，以便于用戶編輯和查閱測(cè)試用例及其執(zhí)行信息。測(cè)試任務(wù)執(zhí)行器ServiceExecutor從測(cè)試用例設(shè)計(jì)器接收測(cè)試任務(wù)，根據(jù)任務(wù)要求展開實(shí)際測(cè)試動(dòng)作，該模塊也可脫離用戶界面，通過腳本驅(qū)動(dòng)。服務(wù)部署容器SvcHost用于發(fā)布待測(cè)服務(wù)和安裝、控制虛擬服務(wù)。代理轉(zhuǎn)發(fā)網(wǎng)關(guān)RedirectProxy用于監(jiān)控不同服務(wù)之間的消息流?？稍诖砭W(wǎng)關(guān)上設(shè)定故障注入或性能控制要求，以控制目標(biāo)服務(wù)的功能和性能表現(xiàn)。

2 約束系統(tǒng)管理

原型工具采用集中管理方式維護(hù)待測(cè)應(yīng)用中的業(yè)務(wù)邏輯約束。圖4展示了工具中的約束管理界面。系統(tǒng)支持23約束求解工具能夠處理的大部分一階邏輯約束公式。為便于結(jié)合Web服務(wù)的特點(diǎn)來表達(dá)約束關(guān)系，測(cè)試工具定義了自己的約束表達(dá)語言，該語言將被翻譯為23約束求解工具接受的約束語言以進(jìn)行約束求解，所得的約束滿足或不滿足解將被翻譯映射回Web服務(wù)上的相關(guān)數(shù)據(jù)，以進(jìn)行測(cè)試。

2.1 約束變量

約束公式建立的基礎(chǔ)是約束變量，系統(tǒng)支持兩種類型的約束變量。

1）值約束變量。其表達(dá)形式為

value（ svc/operation/message_path），

其中value是變量類型名，用以區(qū)分其它類型的約束變量。svc是服務(wù)標(biāo)識(shí)，用以區(qū)分不同的服務(wù)，可通過宏定義方式預(yù)先定義出svc名稱的具體含義。operation是Web服務(wù)的操作的名稱，mes-sage_path是由操作到基本元素參數(shù)的路徑。例如“svc=http： //test.com/axis2/services/Add”表達(dá)add服務(wù)的服務(wù)地址，可通過svc值找到服務(wù)?！皏alue（ svc/add/a）”表達(dá)svc服務(wù)中的add操作的a參數(shù)的取值。

2）時(shí)間約束變量。其形式為

startTime（ svc/operation）

其中startTime是約束變量的類型名稱，整個(gè)約束變量表達(dá)了某一服務(wù)某一操作在服務(wù)調(diào)用過程中的啟動(dòng)時(shí)間。

2.2 約束公式

工具中的約束公式本質(zhì)上是23求解器支持的一階邏輯公式，可以建立在單個(gè)服務(wù)操作的不同參數(shù)之間。包括輸入?yún)?shù)之間，用以表達(dá)輸入數(shù)據(jù)上的限制;也包括輸入和輸出參數(shù)之間，用以描述一個(gè)服務(wù)操作的輸出和輸入之間可能存在的某種聯(lián)系。約束公式還可以建立在不同服務(wù)之間，主要用于描述服務(wù)調(diào)用在時(shí)序上應(yīng)該存在的關(guān)系。典型的約束公式示例如下。

1）值約束。形如

value（ svc/add/a）< value（ svc/add/b），

表達(dá)svc服務(wù)中add操作的a參數(shù)取值應(yīng)小于b參數(shù)取值。

2）時(shí)序約束。形如

startTime（ svc/add）

表達(dá)svc服務(wù)add操作的調(diào)用應(yīng)該在multiple操作之前。

約束用AND、OR、NOT關(guān)系構(gòu)成的樹進(jìn)行組織。樹的葉節(jié)點(diǎn)是基本約束，每個(gè)約束含有一條約束公式?；炯s束通過AND、OR、NOT關(guān)系構(gòu)成更復(fù)雜的約束系統(tǒng)。每個(gè)約束節(jié)點(diǎn)可以命名，以直觀表達(dá)約束的含義。例如

value （svc/add/a）>0 and value （svc/add/a）

表達(dá)svc服務(wù)中add操作包含兩個(gè)基本約束，并通過AND關(guān)系組合成一個(gè)復(fù)雜約束。3 基于約束的服務(wù)單元測(cè)試用例生成

原型工具支持基于約束來生成有效和無效測(cè)試數(shù)據(jù)。針對(duì)每個(gè)待測(cè)服務(wù)操作，可以生成滿足約束的有效測(cè)試數(shù)據(jù)或者不滿足約束的無效測(cè)試數(shù)據(jù)。測(cè)試用例的具體生成流程如圖5所示。首先從待測(cè)項(xiàng)目的整個(gè)約束樹中提取目前所關(guān)注的服務(wù)操作相關(guān)的約束，例如“value（ svc/add/a）+10”.

第二步，建立從服務(wù)操作輸入數(shù)據(jù)到各個(gè)約束變量之間的關(guān)聯(lián)，約束變量的求解結(jié)果即這些參數(shù)將要設(shè)定的取值。然后，利用23求解引擎進(jìn)行約束求解，目前系統(tǒng)支持線性不等式約束、布爾約束、按位運(yùn)算約束、字符串枚舉類型上的判定等約束類型。下一步，根據(jù)求解所獲得的約束變量取值導(dǎo)出服務(wù)操作的參數(shù)取值設(shè)定。最后，根據(jù)參數(shù)取值構(gòu)造服務(wù)操作測(cè)試時(shí)所需的完整SOAP數(shù)據(jù)包，以發(fā)起服務(wù)調(diào)用。

例如，對(duì)于Add服務(wù)規(guī)定add操作規(guī)定參數(shù)值α小于參數(shù)值b，生成滿足約束的測(cè)試數(shù)據(jù)的操作如下。首先提取約束到約束配置界面，給出約束標(biāo)識(shí)svc的值“svc=http：//test.com/axis2/services/Add”及約束表達(dá)式的具體形式其次，“value（ svc/add/a）

測(cè)試用例生成中，基于約束生成無效測(cè)試數(shù)據(jù)的過程與生成有效測(cè)試數(shù)據(jù)的過程非常接近。主要差別在于獲得所有約束后，需要對(duì)約束取反，從而求解獲得違反約束的不合理取值。

在Web服務(wù)中，經(jīng)常需要使用字符串類型，字符串常以枚舉常量形式出現(xiàn)，以作為狀態(tài)標(biāo)識(shí)等。為支持字符串類型上的測(cè)試生成，我們用整數(shù)對(duì)所有出現(xiàn)的字符串常量進(jìn)行編碼，如此，字符串在某一枚舉集中取值、字符串相等、字符串不等等問題，可以轉(zhuǎn)化為整數(shù)上的判等問題，同樣可采用23工具進(jìn)行約束求解。獲得相應(yīng)的解后，我們將整數(shù)編碼重新映射回字符串，可以獲得滿足或不滿足約束要求的字符串。一些字符上常存在正則表達(dá)式表示的模式限制，比如要求密碼字符串的模式為[0-9][0—9][0—9]，表示密碼是三個(gè)數(shù)字構(gòu)成的串。對(duì)此，原型工具使用Xeger程序庫(kù)[13]，借助基于正則表達(dá)式的字符串生成技術(shù)來生成相應(yīng)的滿足或不滿足約束的串。4 基于約束的服務(wù)調(diào)用序列測(cè)試生成

服務(wù)調(diào)用序列可用于檢測(cè)服務(wù)內(nèi)部是否正確實(shí)現(xiàn)了無狀態(tài)特性，不會(huì)因歷史上的其它調(diào)用而影響后續(xù)的服務(wù)執(zhí)行，也可檢測(cè)數(shù)據(jù)是否能夠在相關(guān)服務(wù)操作間有效流轉(zhuǎn)，對(duì)于服務(wù)系統(tǒng)整體的質(zhì)量保證具有重要意義。

在服務(wù)調(diào)用序列測(cè)試中，我們首先需要根據(jù)服務(wù)操作間輸入輸出參數(shù)的匹配情況、多維組合覆蓋要求等，生成用于測(cè)試的候選服務(wù)操作調(diào)用序列。然而，并非上述每一序列對(duì)于實(shí)際測(cè)試均有意義。一個(gè)服務(wù)化應(yīng)用的功能特性可能決定在用戶的使用過程中，A服務(wù)操作的調(diào)用永遠(yuǎn)發(fā)生在B服務(wù)操作之前，這時(shí)測(cè)試A操作發(fā)生于B操作之后的服務(wù)調(diào)用序列顯然意義不大，需要將此類序列進(jìn)行排除。另一類情況下，服務(wù)實(shí)現(xiàn)人員可能認(rèn)為用戶一定先調(diào)用A操作，然后再調(diào)用B操作，而實(shí)際情況中，用戶可能按相反的順序使用。這時(shí)，為測(cè)試服務(wù)系統(tǒng)的健壯性，反而需要測(cè)試B先A后的情況。為支持上述測(cè)試，本測(cè)試工具支持對(duì)服務(wù)操作間的合理調(diào)用時(shí)序進(jìn)行約束建模，然后根據(jù)時(shí)序約束的滿足與不滿足性來生成用于測(cè)試的服務(wù)調(diào)用序列。

服務(wù)調(diào)用序列的生成過程以滿足輸入輸出參數(shù)的類型匹配要求為首要出發(fā)點(diǎn)，首先根據(jù)上述要求生成一批前后服務(wù)調(diào)用間輸入輸出能夠全部或部分銜接的候選序列。然后，根據(jù)約束滿足情況對(duì)這批候選序列進(jìn)行過濾，獲得有效或無效測(cè)試序列。在此基礎(chǔ)上，再根據(jù)組合要求進(jìn)行進(jìn)一步測(cè)試用例選擇。

在檢驗(yàn)一個(gè)候選服務(wù)調(diào)用序列是否滿足業(yè)務(wù)邏輯限定的時(shí)序約束時(shí)，首先從待測(cè)項(xiàng)目的約束系統(tǒng)中，找出相關(guān)服務(wù)操作對(duì)應(yīng)的時(shí)序約束關(guān)系，即一組startTime約束變量上的不等式。例如，如下約束：

startTime（ svc/add）

限定了svc服務(wù)中的add操作一定發(fā)生在其sub操作之前。

然后，將待檢測(cè)的候選序列所蘊(yùn)含的操作間先后關(guān)系也轉(zhuǎn)換為startTime大小關(guān)系加入到約束表中。例如，對(duì)于一個(gè)操作序列，其蘊(yùn)含的時(shí)序約束可以表達(dá)為：startTime（a）

最后，取用戶定義的業(yè)務(wù)邏輯約束和當(dāng)前候選序列中所蘊(yùn)含的先后約束關(guān)系聯(lián)立為不等式組，采用23求解器進(jìn)行約束求解。如果不等式組有解，表明能夠找到各個(gè)服務(wù)操作的startTime（）變量取值，使得無論是用戶的業(yè)務(wù)邏輯要求，還是當(dāng)前序列所要求的順序都能夠得到滿足，當(dāng)前生成的這個(gè)操作序列是合理的;否則表明當(dāng)前操作序列不合理，序列為無效服務(wù)操作調(diào)用序列，對(duì)應(yīng)無效測(cè)試用例。

例如，對(duì)于Calculate服務(wù)，其中的蘊(yùn)含的時(shí)序約束表達(dá)為：“startTime（add）

5 基于約束的故障注入

本服務(wù)化軟件測(cè)試原型工具還支持基于約束的故障注入。故障注入過程首選選擇一批測(cè)試用例作為注入基礎(chǔ)，然后選擇一批注入點(diǎn)來實(shí)施注入。故障注入點(diǎn)以服務(wù)操作進(jìn)行標(biāo)識(shí)。這些服務(wù)操作可以是基礎(chǔ)測(cè)試用例中直接調(diào)用的服務(wù)操作，也可以是基礎(chǔ)測(cè)試用例所調(diào)用的服務(wù)操作內(nèi)部所間接調(diào)用的其它服務(wù)操作。

本測(cè)試系統(tǒng)中，所有的服務(wù)間消息傳遞都經(jīng)過RedirectProxy代理模塊，因此，在該代理中進(jìn)行監(jiān)控，可以比較方便地識(shí)別各個(gè)故障注入點(diǎn)。通過在代理過程中，將原先的正常輸入數(shù)據(jù)替換為異常數(shù)據(jù)，可以注入錯(cuò)誤，檢測(cè)整個(gè)服務(wù)化系統(tǒng)對(duì)于異常的容錯(cuò)情況。

原型系統(tǒng)支持面向消息結(jié)構(gòu)的注入、面向通信的注入、面向業(yè)務(wù)邏輯的注入三種注入方式。面向消息結(jié)構(gòu)的注入主要注入不匹配預(yù)定消息格式的SOAP報(bào)文，如增加無效參數(shù)節(jié)點(diǎn)、刪除有效參數(shù)節(jié)點(diǎn)、參數(shù)節(jié)點(diǎn)亂序等;面向通信的注入主要注入網(wǎng)絡(luò)傳輸故障，如消息重復(fù)、消息丟失、消息亂序的等;而面向業(yè)務(wù)邏輯的注入主要注入結(jié)構(gòu)合法，但數(shù)據(jù)內(nèi)容不滿足業(yè)務(wù)邏輯約束的異常數(shù)據(jù)。

對(duì)于面向業(yè)務(wù)邏輯的故障注入，如果某add服務(wù)正常情況下相關(guān)業(yè)務(wù)邏輯要求其a參數(shù)取值小于b參數(shù)，即：

value（ svc/add/a）< value（ svc/add/b）.

那么，在故障注入中，我們會(huì)對(duì)正常的輸人參數(shù)進(jìn)行篡改，使得α的值大于等于b。如此，可以注入一個(gè)格式正常，但數(shù)據(jù)內(nèi)容通常不會(huì)出現(xiàn)的異常情況。例如，對(duì)于以上約束，我們將通過取反，獲得其否定形式：

not value（ svc/add/a）< value（ svc/add/b）

通過利用SMT求解器求解該約束條件，可以生成一個(gè)違反業(yè)務(wù)邏輯的故障數(shù)據(jù){a=98，b=98）。該故障數(shù)據(jù)可以模擬由于軟硬件錯(cuò)誤造成程序邏輯異常的情況，將更接近真實(shí)場(chǎng)景中可能發(fā)生的故障。測(cè)試用例生成后，故障注入選項(xiàng)選擇“違反取值約束”選項(xiàng)。

故障注入測(cè)試實(shí)施后，系統(tǒng)將報(bào)告測(cè)試執(zhí)行結(jié)果，同時(shí)展示生成的異常報(bào)文，以便于用戶了解容錯(cuò)情況。如圖8所示，Add服務(wù)故障注入前的數(shù)據(jù)是{a=98，b=99），故障注入后的數(shù)據(jù)為{a=869，y=99}，測(cè)試執(zhí)行結(jié)果數(shù)據(jù)為{result=968}。

6 結(jié)論

測(cè)試工具的主要?jiǎng)?chuàng)新點(diǎn)是將約束表達(dá)與求解技術(shù)廣泛應(yīng)用在服務(wù)化軟件的測(cè)試用例生成、故障注入等多個(gè)領(lǐng)域，較之已有工具，具有更強(qiáng)的測(cè)試分析設(shè)計(jì)能力，能夠支持用戶進(jìn)行更高效的測(cè)試。在約束的處理方面，使用了前沿的SMT約束求解技術(shù)，能夠表達(dá)和處理豐富的約束類型，能夠處理不同輸入輸出因素之間的關(guān)聯(lián)性約束，使得更多的業(yè)務(wù)邏輯限制能夠得到有效表達(dá)和處理，從而可以改進(jìn)測(cè)試數(shù)據(jù)的生成質(zhì)量。

對(duì)服務(wù)的約束處理目前支持的約束有值約束和時(shí)序約束可滿足多數(shù)場(chǎng)景下的測(cè)試需求，對(duì)于非線性約束等其他約束值得在未來進(jìn)一步研究。同時(shí)，對(duì)于約束中字符串的處理，當(dāng)前操作使用整數(shù)編碼的形式進(jìn)行處理，未來可以考慮使用23-str進(jìn)行處理。

參考文獻(xiàn)：

[1] LAU Y T.“Service -oriented architecture and the C4ISR frame-work”[J]. The Journal of Defense Software Engineering，2004（9）：11-14

[2]KANKANAMGE C. Web services testing with soapUI[M].Birm-ingham： Packt Publishing Ltd， 2012.

[3]Parasoft SOAtest [EB/OL]（2016-09-27） [2018-03-14]. https：//www.parasoft. com/product/soatest

[4]SOAPSonar [EB/OL] （2018 -02-13） [2018 -03 -14]. http：//www.crosschecknet.com/products/soapsonar.php/

[5]BOZKURT M.HARMAN M.HASSOUN Y.Testing and verifica-tion in service-oriented architecture：a survey[J].Software Test-ing， Verification and Reliability， 2013： 261-313

[6] QIU D， LI B X.JI S H，et al.Regression testing of web service：asystematic mapping study[J].ACM Computing Surveys， 2014， 47（1）：21-46.

[7] HECKEL R，LOHMANN M."Towards contract-based testing ofweb services，”[J].Electronic Notes in Theoretical Computer Sci-ence， 2005， 116（19）： 145-156.

[8]姜瑛，辛國(guó)茂，單錦輝，等.一種Web服務(wù)的測(cè)試數(shù)據(jù)自動(dòng)生成方法[J]計(jì)算機(jī)學(xué)報(bào).2005 （4）：568-577.

[9]侯可佳，白曉穎，陸?zhàn)?，等，基于接口語義契約的Web服務(wù)測(cè)試數(shù)據(jù)生成[J].軟件學(xué)報(bào)，2013.24（9）：2020-2041.

[10]HOU J，ZHOU H， MA C， et al.Method for automatically generat-ing test cases for web services[J].Journal of Northwestem Poly-technic al University， 2018， 36（1）：149-155.

[11]王翀，呂蔭潤(rùn)，陳力，等.SMT求解技術(shù)的發(fā)展及最新應(yīng)用研究綜述[J].計(jì)算機(jī)研究與發(fā)展，2017，54（07）：1405-1425.

[12] MOURA LD，BJRNERN."23： An efficient SMT solver，”[C].in Proceedings of the Intemational conference on Tools and Algo-rithms for the Construction and Analysis of Systems， 2008： 337-340

[13]XEGER[EB/OL]（ 2017 -06 -24） [2018 -03 -19]. https： //github.com/bluezio/xeger.