從BPMN 模型導(dǎo)出組合服務(wù)的代數(shù)規(guī)約＊

余 波

（1.中南林業(yè)科技大學(xué)涉外學(xué)院，湖南 長沙410042；2.國防科學(xué)技術(shù)大學(xué)計算機學(xué)院，湖南 長沙 410073）

1 引言

目前，越來越多的復(fù)雜商業(yè)應(yīng)用解決方案采用諸如BPEL（Business Process Execution Language）、WSFL（Web Services Flow Language）、XLang（an XML-based extension of Web Services Description Language）等組合服務(wù)編程語言，將多個基本或組合服務(wù)組織成能夠完成業(yè)務(wù)過程自組的程序。BPEL已經(jīng)成為基于Web服務(wù)開發(fā)可執(zhí)行業(yè)務(wù)流程的標(biāo)準(zhǔn)之一[1]。業(yè)務(wù)流程建模標(biāo)注BPMN（Business Process Modeling Notation）是一種獨立于其它流程建模方法的流程建模標(biāo)準(zhǔn)，提供了一套用戶易于理解的圖形符號和在BPEL 流程建模及其實現(xiàn)之間平滑過渡的有效機制[2]。

Web服務(wù)的質(zhì)量受到高度關(guān)注。與模型檢驗等方法相比，軟件測試是一種發(fā)現(xiàn)Web服務(wù)缺陷或者錯誤的簡便方法。即使參與組合的Web服務(wù)在發(fā)布之前均經(jīng)過測試，仍然需要檢查BPEL程序的可執(zhí)行服務(wù)組合邏輯是否正確，以及BPEL服務(wù)與其它Web 服務(wù)組合時是否存在缺陷。由于Web服務(wù)對外僅提供被調(diào)用的接口信息，隱藏源代碼甚至可執(zhí)行代碼，因此Web服務(wù)測試需要采用基于規(guī)約的測試方法[3]。

代數(shù)規(guī)約技術(shù)出現(xiàn)于20世紀(jì)70年代，定義抽象數(shù)據(jù)類型時具有獨立于實現(xiàn)的特點，并且以公理集刻畫抽象數(shù)據(jù)類型的代數(shù)語義?；诖鷶?shù)規(guī)約的測試方法獨立于軟件系統(tǒng)的設(shè)計與實現(xiàn)，具有自動生成測試用例、判斷測試輸出和提供測試驅(qū)動等優(yōu)點，已經(jīng)成功地應(yīng)用于測試抽象數(shù)據(jù)類型、過程、類、組件和Web服務(wù)等[4～6]。

應(yīng)用代數(shù)測試方法測試組合Web服務(wù)時，首先需要解決Web服務(wù)的代數(shù)規(guī)約生成問題。文獻[7]提出以統(tǒng)一風(fēng)格描述抽象數(shù)據(jù)類型、過程、類、組件與Web 服務(wù)描述語言WSDL（Web Service Definition Language）定義的Web服務(wù)的代數(shù)規(guī)約語言CASOCC-WS（Common Algebraic Specification Language of Component and Class for Web Service），給出了由基本W(wǎng)eb服務(wù)的WSDL 描述轉(zhuǎn)換成代數(shù)規(guī)約的方法。

本文通過建立BPMN 結(jié)構(gòu)化表示與正則表達式的映射規(guī)則，設(shè)計由BPMN 模型導(dǎo)出BPEL 服務(wù)的以CASOCC-WS表示的代數(shù)規(guī)約算法。文章結(jié)構(gòu)組織如下：第2節(jié)介紹CASOCC-WS；第3節(jié)介紹BPMN 及其轉(zhuǎn)換成基調(diào)的映射規(guī)則；第4節(jié)介紹由正則表達式導(dǎo)出項的算法和書寫公理等式的啟發(fā)式規(guī)則；第5節(jié)介紹一個案例；第6節(jié)介紹相關(guān)研究工作；最后總結(jié)全文。

2 代數(shù)規(guī)約語言

描述Web 服務(wù)的代數(shù)規(guī)約語言CASOCCWS[7]以描述抽象數(shù)據(jù)類型、類和組件的代數(shù)規(guī)約語言CASOCC[4]為基礎(chǔ)，兩者在語法和語義上基本相同。主要區(qū)別在于：后者將操作分為創(chuàng)建子（Creator）、構(gòu)造子（Constructor）、轉(zhuǎn)換子（Transformer）和觀察子（Observer）四類；前者將操作分為觀察子、創(chuàng)建子和構(gòu)造子，構(gòu)造子部分可選。CASOCC-WS使用的字符集與Java語言的相同。標(biāo)識符以字母或下劃線開頭，連接大小寫字母、數(shù)字和下劃線。保留字包括預(yù)定義的基本數(shù)據(jù)類型、Spec、Import、Operations、Var、Axioms、Constructor、Observer和Transformer等。

一個軟件系統(tǒng)的代數(shù)規(guī)約除了定義數(shù)據(jù)和操作的基調(diào)（Signature）外，另一個重要組成部分是刻畫軟件系統(tǒng)行為屬性的公理集合[8]。CASOCCWS描述Web服務(wù)的基本單位是規(guī)約單元，以關(guān)鍵字“Spec”開始、“End”結(jié)束；“Observable”后附帶“F”表示該代數(shù)規(guī)約不可觀察或者“T”表示可觀察；“Import”后附帶引入的類子或者其它分類；“Operations”部分依次是構(gòu)造子、轉(zhuǎn)換子和觀察子的定義；“Axioms”部分描述公理等式；“Vars”部分描述公理中出現(xiàn)的變量。類子即基本類型的分類。XML Schema定義的數(shù)據(jù)類型即為預(yù)定義類子。

代數(shù)規(guī)約SP＝〈Σ，E〉，基調(diào)SI＝〈S，F(xiàn)〉，s1，…，sn，O 是S 的引入分類，且O 是可觀察分類，si≠S，0≤i≤n，f 是S 中的操作，0≤k≤n；如果f：s0×…×sk→S，則稱f為創(chuàng)建子；如果f：S×s0×…×sk→S，則稱f為轉(zhuǎn)換子：如果f：S×s0×…×sk→O，則稱f為觀察子?；{(diào)定義的分類稱為主分類。如果x的類型是主分類，操作f作用于參數(shù)x 和y，則可記成x.f（y）。

一個項由Var部分聲明的變量、Operations部分聲明或被引入分類的操作或常數(shù)構(gòu)成。一個公理等式包含標(biāo)號、等式和可選條件三個部分。一個等號連接兩個項就構(gòu)成一個公理等式。等式中每個包含操作的項由構(gòu)造子或者以主分類類型聲明的變量開始，連接轉(zhuǎn)換子，最后以觀察子結(jié)束。條件可以是布爾型的項、等式以及邏輯關(guān)系式。

代數(shù)測試方法的基本思想是，以常數(shù)替代公理等式的項的變量，使得該項成為基礎(chǔ)項。一條公理包含兩個相等的基礎(chǔ)項，包含操作的項又能看成是操作所構(gòu)成的調(diào)用序列[5]。因此，測試用例可看作是一個三元組〈T1，T2，Cond〉，T1 和T2 是基礎(chǔ)項，Cond 表示具有Boolean類型的條件，該條件可選。當(dāng)Cond 為空或者其真值為真時，T1和T2的值應(yīng)該相等。如果不等，則認(rèn)為該公理所包含的操作中至少存在一個錯誤。

若Ai是代數(shù)規(guī)約的一條公理，記LSet＝｛f：s0×…×sk→S｜f在Ai的等號左邊的項中出現(xiàn)｝，RSet＝｛f：s0×…×sk→S｜f在Ai的等號右邊的項中出現(xiàn)｝，若LSet∩RSet＝?，則稱Ai是第一類公理。若RSet退化為變量和常量的基本運算表達式，則Ai是包含泛不動點的公理[6]。如果f ∈LSet∩RSet，且f 中包含錯誤，則該公理可能檢測不出。

3 業(yè)務(wù)流程建模符號

BPMN 圖形元素分為流對象、連接對象、泳道和物件四類。流對象定義業(yè)務(wù)流程；連接對象用于描述流對象間的連接以及建立流對象與物件的關(guān)聯(lián)；泳道用于對基本建模元素分組；物件描述流程的額外信息。BPMN 規(guī)范還規(guī)定到BPEL 程序的映射。已有多個工具提供BPMN 建模環(huán)境。通常以XML來表示應(yīng)用BPMN 元素建立的組合服務(wù)模型。

一個BPEL程序的BPMN 模型是一個有向圖G＝〈N，E，Start，Exit〉，節(jié)點集合N 中的每個元素是一個BPMN 中的業(yè)務(wù)流程；邊集E 中的每個元素e＝〈n1，n2〉表示從節(jié)點n1到節(jié)點n2有一條有向邊，邊即連接對象表示的業(yè)務(wù)流程間的關(guān)系；Start和Exit分別表示子程序的入口和出口節(jié)點，Start，Exit∈N。

3.1 轉(zhuǎn)換規(guī)則

BPMN 表示轉(zhuǎn)換成基調(diào)的規(guī)則定義如下：

（1）BPMN 的名稱對應(yīng)代數(shù)規(guī)約的名稱。

（2）對于BPMN 包含的每個消息或者類型定義，如果未曾定義其代數(shù)規(guī)約，則按文獻[7]的類型或者消息轉(zhuǎn)換成代數(shù)規(guī)約的規(guī)則轉(zhuǎn)換之，生成的代數(shù)規(guī)約的分類名即為該類型的類型名或者消息名；將生成的代數(shù)規(guī)約的分類名添加至基調(diào)的Import列表中。

（3）BPMN中的每個操作和數(shù)據(jù)類型可映射為基調(diào)中的操作的對應(yīng)定義，即BPMN 定義的每個操作對應(yīng)基調(diào)的一個操作定義；如果返回類型是可觀察類型，則將該操作添加至基調(diào)的Observer部分；否則添加至Transformer部分；操作的每個輸入?yún)?shù)類型，如果沒有在Import列表中出現(xiàn)過，則添加至Import列表；對于每個返回類型，如果沒有在Import列表中出現(xiàn)過，則添加至Import列表。

3.2 從BPMN 結(jié)構(gòu)到基調(diào)的映射規(guī)則

假定BPMN 圖中節(jié)點N 采用五元組〈no，op，ic，oc，nl〉表示，其中，no 表示節(jié)點編號，op 表示操作語句，ic表示節(jié)點的入度，oc表示節(jié)點的出度，nl是鏈接后繼節(jié)點的指針。節(jié)點表示流程中的任務(wù)、嵌入式流程、啟動事件、中間事件、結(jié)束事件和網(wǎng)關(guān)。圖1～圖6所用運算符號的含義如下：

（1）a；b：表示順序執(zhí)行操作a和操作b；

（2）a＊：表示循環(huán)執(zhí)行操作a零次或者多次；

（3）！con＿1：表示對條件con＿1取非；

（4）a｜b：表示并行執(zhí)行操作a和操作b；

（5）a[]b：表示選擇地執(zhí)行操作a和操作b之一；

（6）（a；b）：表示順序執(zhí)行操作a和操作b。

其中，a、b等符號表示操作名，“｛｝”包含的表達式con＿1、con＿2等表示條件。由“；”、“＊”、“！”、“｜”、“[]”、“（）”等運算構(gòu)成的正則表達式表示一個復(fù)合節(jié)點。圖1～圖6分別給出上述六個運算對應(yīng)到正則表達式的轉(zhuǎn)換規(guī)則。

3.2.1 順序合并規(guī)則

如果節(jié)點a的出度及其直接后繼節(jié)點b和c的入度均等于1，則該結(jié)構(gòu)可合并為新節(jié)點d，d.no＝a.no＿b.no＿c.no，d.op＝a.op；b.op；c.op，d.ic＝a.ic，d.oc＝c.oc，d.nl＝c.nl。如圖1所示。

Figure 1 Rule for sequence圖1 順序流合并規(guī)則

3.2.2 條件流合并規(guī)則

如果節(jié)點a具有兩個不同取值，b和d 分別對應(yīng)a 的不同取值可執(zhí)行的活動或者消息，而且d 還表示條件歸并節(jié)點，則該結(jié)構(gòu)可合并為新節(jié)點f，f.no＝a.no＿b.no＿c.no＿d.no；f.op＝（a；d）[]（a；b；c；d），f.ic＝a.ic，f.oc＝d.oc，f.nl＝d.nl。如圖2所示。

Figure 2 Rule for choice圖2 條件結(jié)構(gòu)合并規(guī)則

3.2.3 異或網(wǎng)關(guān)合并規(guī)則

如果節(jié)點a表示具有多個數(shù)據(jù)或者事件取值的網(wǎng)關(guān)，b、c、d 分別對應(yīng)a 的不同取值的活動或消息，e表示異或歸并節(jié)點，則該結(jié)構(gòu)可合并為一個新節(jié)點f，f.no＝a.no＿b.no＿c.no＿d.no＿e.no；f.op＝a；（｛c1｝b[]｛c2｝c[]｛c3｝d）；e，f.ic＝a.ic，f.oc＝e.oc，f.nl＝e.nl。如圖3所示。

Figure 3 Rule for XOR圖3 異或網(wǎng)關(guān)合并規(guī)則

3.2.4 循環(huán)結(jié)構(gòu)合成規(guī)則（循環(huán)體至少執(zhí)行一次）

節(jié)點a表示具有多個數(shù)據(jù)或者事件取值的網(wǎng)關(guān)，b、c 分別表示可循環(huán)執(zhí)行的順序節(jié)點，節(jié)點d表示具有多個數(shù)據(jù)或者事件取值的網(wǎng)關(guān)節(jié)點，則該結(jié)構(gòu)可以合并為一個新節(jié)點e，e.no＝a.no＿b.no＿c.no＿d.no；e.op＝a；b；c；（d；a；b；c）＊[]！d.e.ic＝a.ic，e.oc＝d.oc，e.nl＝d.nl。如圖4所示。

Figure 4 Rule for loop（loop body executed more than once）圖4 循環(huán)結(jié)構(gòu)合并規(guī)則（循環(huán)體至少執(zhí)行一次）

3.2.5 循環(huán)結(jié)構(gòu)合成規(guī)則

節(jié)點a表示具有多個數(shù)據(jù)或者事件取值的網(wǎng)關(guān)，b、c分別表示循環(huán)體內(nèi)的順序節(jié)點，d 表示網(wǎng)關(guān)的另外一個分支節(jié)點，則該結(jié)構(gòu)可以合并為一個新節(jié)點e，e.no＝a.no＿b.no＿c.no＿d.no；e.op＝a；（b；c）＊[]！a；d；e.ic＝a.ic，e.oc＝d.oc，e.nl＝d.nl。如圖5所示。

3.2.6 與網(wǎng)關(guān)合并規(guī)則

節(jié)點a表示具有多個數(shù)據(jù)或者事件取值的網(wǎng)關(guān)，b、c分別對應(yīng)兩個并行的節(jié)點，d 表示與歸并節(jié)點，則該結(jié)構(gòu)可以合并為一個新節(jié)點e，e.no＝a.no＿b.no＿c.no＿d.no；e.op＝a；（b｜c）；d，e.ic＝a.ic，e.oc＝e.oc，e.nl＝d.nl。如圖6所示。

Figure 5 Rule for loop（Loop body may not execute）圖5 循環(huán)結(jié)構(gòu)合成規(guī)則（循環(huán)體可以一次不執(zhí)行）

Figure 6 Rule for AND gate圖6 與網(wǎng)關(guān)合并規(guī)則

一個BPMN 模型可以看作是一個圖G，因此由圖G 導(dǎo)出正則表達式的算法如下所述。

算法1 由圖導(dǎo)出操作表達式算法

步驟1 遍歷BPMN 文檔，以操作名和條件名為節(jié)點構(gòu)建圖G。

步驟2 深度優(yōu)先遍歷圖G，依次識別單入口單出口節(jié)點，根據(jù)規(guī)則3.2.1合并圖G。

步驟3 深度優(yōu)先遍歷圖G，根據(jù)節(jié)點間關(guān)系，對于單入口多出口結(jié)點，按規(guī)則3.2.2、3.2.3、3.2.6合并圖G；對于多入口單出口結(jié)點，按規(guī)則3.2.4和3.2.5合并圖G。

步驟4 深度遍歷圖G，如果圖G 已經(jīng)合并成一個復(fù)合節(jié)點，則結(jié)束算法；否則，依次執(zhí)行步驟2～步驟4。

顯然，執(zhí)行上述算法，圖G 最終會合并成一個僅僅包含“（）”、“｜”、“＊”、“！”、“[]”、“；”、操作名和條件名的正則表達式節(jié)點。

如果一個BPMN 程序僅僅包含順序、循環(huán)、選擇和并行等四種結(jié)構(gòu)，則算法1的執(zhí)行時間是有限的。假設(shè)BPMN 模型的操作節(jié)點數(shù)為n，條件節(jié)點數(shù)為m，且m＜n，則算法1 的時間復(fù)雜度是O（n2）。

3.3 由正則表達式導(dǎo)出公理

從包含“（）”、“｜”、“＊”、“！”、“[]”、“；”等連接符的正則表達式導(dǎo)出操作調(diào)用序列，主要步驟即先先將循環(huán)和并行運算轉(zhuǎn)化成由“[]”表示的正則表達式，然后應(yīng)用算法2從每個“[]”運算正則表達式中抽取一個選擇項以構(gòu)成操作序列。

3.3.1 循環(huán)運算

對于一個包含“＊”運算的正則表示a＊，其中a為操作，如果a至少出現(xiàn)一次，則a＊可以表示成a[]（a；a）[]（a；a；a）[]，否則可以將其表示成（）[]a[]（a；a）[]…，其中，“（）”表示空操作。如果操作a的循環(huán)次數(shù)為k，則選擇運算表示的正則表達式的最后一個項即為操作a執(zhí)行k 次。

3.3.2 并行運算

對于一個包含“｜”運算的正則表示a｜b，a、b均為操作，則可表示成a；b[]b；a。

3.3.3 選擇運算

只包含一個選擇運算符“[]”的正則操作表達式a[]b，表示分別選擇a 或者b 操作；如果包含多個“[]”運算符號，在生成操作調(diào)用序列時，由“[]”連接的每個操作均可以被選擇一次。

3.3.4 生成操作調(diào)用序列

對于由算法1 所導(dǎo)出的正則表達式，按照3.2.1和3.2.2節(jié)的規(guī)則將循環(huán)和并行操作轉(zhuǎn)換成由“[]”連接的表達式，算法描述略。

下面介紹由“[]”和操作構(gòu)成的正則表達式生成操作調(diào)用序列的算法。節(jié)點數(shù)據(jù)結(jié)構(gòu)和指向該操作或者條件的后續(xù)節(jié)點中的第一個節(jié)點、指向同一層級的“[]”連接的兄弟節(jié)點和指向該節(jié)點有前驅(qū)節(jié)點的指針，另外一個用于記錄節(jié)點被遍歷次數(shù)的域count，一個僅僅包含“[]”運算的正則表達式由鏈表數(shù)組表示。

算法2 僅包含選擇操作的表達式生成操作調(diào)用序列

根據(jù)前面有關(guān)操作節(jié)點與條件節(jié)點個數(shù)的假設(shè)，算法2的時間復(fù)雜度為O（nm）。

3.4 由項導(dǎo)出公理的啟發(fā)式規(guī)則

每個序列可以看作是等式的一個項。對于每個由算法2導(dǎo)出的項，按下面的規(guī)則處理。

（1）從根出發(fā)，執(zhí)行算法1，構(gòu)造從根至終端節(jié)點形如｛p1｝t1…｛pi｝ti｛pi＋1｝ti＋1…｛pn｝tn｛pn＋1｝的序列seq。

（2）對于每個序列seq，從其包含的謂詞處分開，構(gòu)造如下形式的公理：“｛p1｝t1…｛pi｝＝true，if p1＆＆…＆＆pi；”…；“｛p1｝t1…｛pi｝ti｛pi＋1｝＝true，if p1＆＆…＆＆pi＋1；”…“｛p1｝t1…｛pi｝ti｛pi＋1｝ti＋1…｛pn｝tn｛pn＋1｝，if p1＆＆ …＆＆pn＋1；”。

（3）如果一個形如｛p1｝t1…｛pi｝ti｛pi＋1｝ti＋1…｛pn｝tn｛pn＋1｝的序列seq 包含一個觀察子ti，則可構(gòu)造如下形式的公理：｛p1｝t1…｛pi｝ti＝aValue；aValue是人工分析該序列得到的一個表達式或者值，“｛p1｝t1…｛pi｝”是ti的可觀察上下文。

（4）如果所定義的基調(diào)中的每個改變待測試軟件實體的狀態(tài)操作對應(yīng)一個將所改變狀態(tài)還原到該操作執(zhí)行前的狀態(tài)的還原操作，則需要在這些操作執(zhí)行后，逆序添加還原操作，將Web服務(wù)的狀態(tài)恢復(fù)到執(zhí)行測試之前的狀態(tài)。

（5）如果所定義的基調(diào)的改變狀態(tài)的操作沒有對應(yīng)的還原操作，則包含該操作的序列寫在公理等式等號的右邊，而等式等號的左邊書寫不改變狀態(tài)的序列、表達式或者常值。

上述規(guī)則（4）和規(guī)則（5）可以避免在執(zhí)行一次包含兩個序列的測試時，前一次測試序列執(zhí)行對后面的測試序列的執(zhí)行結(jié)果產(chǎn)生副作用。

4 原型工具與案例研究

根據(jù)上述算法和規(guī)則生成的操作調(diào)用序列，可以用于構(gòu)造公理等式等號左邊的項，等號右邊的項須由人工完成。從BPMN 模型導(dǎo)出基調(diào)的原型工具以BPMN 建模文件（XML文件）為輸入，生成由CASOCC-WS描述的組合服務(wù)的代數(shù)規(guī)約框架，而公理等式則需要由測試員補充完整。

Jboss公司發(fā)布的組合服務(wù)引擎Jbpel附帶一個組合服務(wù)ATM 示例[9]，其部署環(huán)境：Windows XP＋JDK1.5＋Jboss4.2.0 ＋JBPM1.1。ATM服務(wù)的BPMN 模型如圖7所示。根據(jù)以上規(guī)則，可得到如下形式代數(shù)規(guī)約，其中公理由人工完成。

該代數(shù)規(guī)約僅給出ATM 的部分操作的定義和部分公理，公理表示中“｛…｝”包含前置或后置條件。FrontEnd、Account和TicketIssuer的代數(shù)規(guī)約在此省略。在公理5中，執(zhí)行操作F.withdraw（y，d）會改變Web服務(wù)的狀態(tài)，在該公理的等號右邊的項的后置條件部分添加操作F.deposit（y，d），以還原操作F.withdraw（y，d）對Web服務(wù)的狀態(tài)變化。

5 相關(guān)工作

BPEL 程序測試分為單元測試和集成測試[10]。BPEL 組合服務(wù)的測試需要解決如下問題：（1）自動生成測試數(shù)據(jù)或者測試用例；（2）一個自動運行測試的驅(qū)動程序；（3）測試結(jié)果判定問題等。已有BPEL測試的工作主要有如下幾類：（1）基于模型驗證器的測試方法，如測試BPEL服務(wù)的一致性[8]；（2）基于BPEL程序結(jié)構(gòu)測試方法，如應(yīng)用數(shù)據(jù)流測試BPEL 程序[11，12]，基于圖的遍歷測試BPEL 程序[13]；（3）基于已有測試框架測試BPEL程序[14]；（4）基于形式化規(guī)約測試BPEL 程序[15]等。這些工作主要解決測試數(shù)據(jù)生成或者測試驅(qū)動，對于測試輸出的自動判斷還是沒有提供適當(dāng)?shù)慕鉀Q方案[16]。

Figure 7 BPMN model of ATM圖7 ATM 的BPMN 模型表示

6 結(jié)束語

為了解決應(yīng)用代數(shù)規(guī)約測試BPEL 組合服務(wù)的代數(shù)規(guī)約生成問題，本文提出了從BPMN 模型導(dǎo)出BPEL服務(wù)的用代數(shù)規(guī)約語言CASOCC-WS表示的代數(shù)規(guī)約的方法。該方法可從BPMN 模型中自動導(dǎo)出基調(diào)，提出的書寫代數(shù)規(guī)約的啟發(fā)式規(guī)則，可方便測試員書寫代數(shù)規(guī)約。將來的工作包括：進一步改進提出的方法，實現(xiàn)基于代數(shù)規(guī)約自動測試BPEL服務(wù)的工具。

[1]IBM.Business process execution language for Web services version 1.1[EB／OL].[2010-06-28].http：／／www.ibm.com／developerworks／library／specification／ws-bpel／.

[2]OMG.Documents associated with business process model and notation（BPMN）1.2[EB／OL].[2010-07-13].http：／／www.omg.org／spec／BPMN／1.2／PDF／.

[3]Jokhio M S，Dobbie G，Sun J.Towards specification based testing for semantic Web services[C]∥Proc of 2009Australian Software Engineering Conference，2009：54-63.

[4]Kong Liang，Zhu Hong，Zhou Bin.Automated testing EJB components based on algebraic specifications[C]∥Proc of COMPSAC'07，2.07：717-722.

[5]Yu Bo，Kong Liang，Zhang Yu-feng，Zhu Hong.Testing java components based on algebraic specifications[C]∥Proc of ICST'08，2.08：190-199.

[6]Yu Bo，Kong Liang，Peng Chen.Web service test based on algebraic specification[J].Computer Engineering，2009，35（21）：60-61.（in Chinese）

[7]Zhu H，Yu Bo.Algebraic specification of Web service[C]∥Proc of the 10th International Conference on Quality Software，2010：457-464.

[8]Dong Rong-sheng，Wei Zhao，Luo Xiang-yu，et al.Testing conformance of BPEL business process based on model checking[J].Journal of Software，2010，5（9）：1030-1037.

[9]Jboss.WS-BPEL runtime user guide[EB／OL].[2007-11-29].http：／／docs.jboss.com／jbpm／bpel／v1.1／userguide／tutorial.atm.html.

[10]Mayer P.Towards a BPEL unit testing framework[C]∥Proc of International Symposium on Software Testing and Analysis，2006：33-42.

[11]Liu Chien-hung，Chen Shu-ling.Data flow analysis and testing for web service compositions based on WS-BPEL[C]∥Proc of SEKE'09，2.09：306-311.

[12]Mei Li-jun，Chan W K，Tse T H，et al.An empirical study of the use of frankl-weyuker data flow testing criteria to test bpel web services[C]∥Proc of International Computer Software and Applications Conference，2009：81-88.

[13]Yuan Yuan，Li Zhong-jie，Sun Wei.A graph-search based approach to BPEL4WS test generation[C]∥Proc of International Conference on Software Engineering Advances，2006：14-14.

[14]Li Z J，Tan H F，Liu H H，et al.Business-process-driven gray-box SOA testing[J].IBM Systems Journal，2008，47（3）：457-472.

[15]Ma Chun-yan，Wu Jun-sheng，Zhang Tao，et al.Testing BPEL with stream X-machine[C]∥Proc of International Symposium on Information Science and Engineering，2008：578-582.

[16]Ladan，Mohamad I.Web services testing approaches：A survey and a classification[J].Communications in Computer and Information Science，2010，88（2）：70-79.

附中文參考文獻：

[6]余波，孔良，彭琛.基于代數(shù)規(guī)約測試Web服務(wù)的工具的設(shè)計與實現(xiàn)[J].計算機工程，2009，35（21）：60-61.