一種Web服務(wù)組合一致性驗(yàn)證方法研究

馬薇薇　王進(jìn)　姜家鑫

摘要：為解決Web服務(wù)組合事務(wù)放松ACID屬性后，原子性與一致性無法保證同時(shí)滿足的問題，提出了一種基于有限狀態(tài)自動(dòng)機(jī)的服務(wù)組合概念一致性檢測(cè)方法。與以往大多通過運(yùn)行時(shí)監(jiān)控和協(xié)調(diào)保證應(yīng)用一致性的方法不同，該方法采用有限狀態(tài)自動(dòng)機(jī)在設(shè)計(jì)階段對(duì)服務(wù)組合的交互行為與異常處理進(jìn)行建模，分析了概念一致性滿足的關(guān)鍵條件和性質(zhì)，證明了服務(wù)組合概念一致性的判定定理。最后通過分析服務(wù)組合一致性檢測(cè)的實(shí)施框架說明了該方法的可行性。

關(guān)鍵詞：Web服務(wù)組合；確定有限狀態(tài)自動(dòng)機(jī)；事務(wù)；一致性檢測(cè)

中圖分類號(hào)：TP311文獻(xiàn)標(biāo)識(shí)碼：A

Abstract：To solve the problem that atomicity and consistency cannot be guaranteed to satisfy at the same time when ACID properties are relaxed in Web services composition transaction.A Deterministic Finite State Automata（DFA） based approach is presented to check the conceptual consistency in services composition.Different from most previous works which keep application consistency by runtime monitoring and coordination，this approach uses DFA to model interaction behavior and exception handling process of services composition at design stage.The DFA based approach analyzes the key conditions and properties to satisfy the conceptual consistency；and further，it proofs the theorem to determine the conceptual consistency in service composition.Finally，by analyzing the deployment framework of services composition consistency detection，the feasibility of our approach has been illustrated.

Key words：Web services；DFA；transaction；consistency checking

1引言

面向服務(wù)計(jì)算模式（SoC）以可重用服務(wù)為構(gòu)造單元，為解決分布式應(yīng)用集成提供了新型計(jì)算范型[1，2]。服務(wù)作為自治、自描述和平臺(tái)獨(dú)立的模塊化應(yīng)用[3]。為企業(yè)間協(xié)作提供了協(xié)作基礎(chǔ)。但單個(gè)服務(wù)本身功能單一，無法提供完整解決方案。因此，必須對(duì)服務(wù)進(jìn)行組合和協(xié)作以實(shí)現(xiàn)復(fù)雜B2B業(yè)務(wù)邏輯[4，5]。Web服務(wù)資源自治性高，潛在故障多，可長(zhǎng)期運(yùn)行等特點(diǎn)引發(fā)了Web服務(wù)組合協(xié)作的一系列新需求（如死鎖處理，兼容性檢測(cè)等）。這其中，保持服務(wù)組合后應(yīng)用一致性是一個(gè)關(guān)鍵問題[6，7]。在Web服務(wù)組合中引入事務(wù)概念，利用事務(wù)“非全則無”的語(yǔ)義可以有效增強(qiáng)服務(wù)組合的可靠性，保障參與組合數(shù)據(jù)與應(yīng)用自身狀態(tài)的一致。但Web服務(wù)由于其運(yùn)行長(zhǎng)周期，異構(gòu)等特點(diǎn)，不可能按照傳統(tǒng)事務(wù)嚴(yán)格鎖定的方式來管理資源。對(duì)傳統(tǒng)事務(wù)的ACID屬性進(jìn)行適當(dāng)放松成為必然。

在Web 服務(wù)組合事務(wù)模型中，主要通過異常處理這樣一種相對(duì)柔性的方式來達(dá)到概念上的原子性與一致性[8，9]。文獻(xiàn)[10]提出的Saga模型是最早應(yīng)用于Web事務(wù)領(lǐng)域的事務(wù)模型之一。Saga模型將一個(gè)完整事務(wù)分解為若干個(gè)子事務(wù)，并為每個(gè)子事務(wù)設(shè)計(jì)業(yè)務(wù)邏輯上相對(duì)應(yīng)的補(bǔ)償事務(wù)，在失效情況下，執(zhí)行失效部分的補(bǔ)償事務(wù)以達(dá)到語(yǔ)義上的一致性與原子性。文獻(xiàn)[11]提出的全局事務(wù)模型對(duì)Saga模型進(jìn)行進(jìn)一步擴(kuò)展，提出全局回滾以及局部回滾的概念來處理不同失效場(chǎng)景。在Saga模型與全局事務(wù)模型中，都嚴(yán)格要求對(duì)失效的操作進(jìn)行補(bǔ)償。實(shí)際應(yīng)用場(chǎng)景中，往往對(duì)于某些子事務(wù)操作由于補(bǔ)償代價(jià)過高而無法真正進(jìn)行補(bǔ)償。文獻(xiàn)[12]針對(duì)單一補(bǔ)償方式的不足，提出了后向補(bǔ)償與前向的替換（重試）相結(jié)合的異常處理方式，這一處理方式在目前服務(wù)組合事務(wù)處理相關(guān)研究中被廣泛采納。

文獻(xiàn)[13]在文獻(xiàn)[12]的基礎(chǔ)上，通過定義服務(wù)組合原子范圍（atomicity sphere）實(shí)現(xiàn)業(yè)務(wù)流程放松的原子性要求。在此種半原子性模型中，每個(gè)子事務(wù)都具備可補(bǔ)償性與可重試性這兩個(gè)正交屬性。該模型可在參與業(yè)務(wù)流程的服務(wù)未隱藏業(yè)務(wù)細(xì)節(jié)時(shí)，檢查流程的原子范圍，構(gòu)建可靠的組合服務(wù)。文獻(xiàn)[14]使用進(jìn)程代數(shù)對(duì)服務(wù)組合進(jìn)行了建模，并通過引入公理系統(tǒng)的方式，檢測(cè)組合的原子范圍。但其公理系統(tǒng)主要是為順序和選擇結(jié)構(gòu)提供規(guī)約，對(duì)并發(fā)情況下的交錯(cuò)時(shí)序考慮較少。文獻(xiàn)[13，14]中所采用的半原子性模型，不能保證組合事務(wù)在符合放松的原子性時(shí)同時(shí)滿足一致性。文獻(xiàn)[15]針對(duì)以上的事務(wù)模型進(jìn)一步提出了面對(duì)長(zhǎng)周期事務(wù)的調(diào)度算法和層次式失效恢復(fù)算法.這些研究主要集中于在運(yùn)行期間通過協(xié)調(diào)和調(diào)度保證最終結(jié)果的一致性，對(duì)設(shè)計(jì)階段一致性檢測(cè)少有涉及。文獻(xiàn)[16]提出集合一致性（set consistency）的概念來檢測(cè)設(shè)計(jì)時(shí)的一致性，但該方法需要用戶定義一致性滿足條件。這種一致性條件更多反映的是業(yè)務(wù)需求上的一種約束，對(duì)事務(wù)概念層上的一致性難以描述。

針對(duì)以上研究中的不足，本文試圖給出一種針對(duì)原子范圍理論原子性定義下的服務(wù)組合建模方法。endprint

本文首先結(jié)合案例分析了服務(wù)組合一致性檢測(cè)問題的產(chǎn)生，對(duì)服務(wù)組合的交互行為及其異常行為進(jìn)行基于確定有限狀態(tài)自動(dòng)機(jī)的建模。針對(duì)建立的異常行為模型，提出并證明了概念一致性的判定定理。并且考慮到服務(wù)組合異常模型可能產(chǎn)生的狀態(tài)爆炸問題，進(jìn)一步提出了對(duì)異常行為模型的約簡(jiǎn)方法。

2服務(wù)組合一致性問題及其建模

21Web服務(wù)組合一致性問題描述

與傳統(tǒng)嚴(yán)格鎖定的事務(wù)ACID屬性必然同時(shí)滿足不同，在異常處理方式中，事務(wù)滿足原子范圍并不能保證其同時(shí)滿足一致性要求。根據(jù)事務(wù)自身一致性的定義可知，服務(wù)組合事務(wù)滿足事務(wù)概念上的一致性應(yīng)保證任意事務(wù)執(zhí)行路徑上的子事務(wù)出現(xiàn)異常時(shí)，通過異常處理及后續(xù)一系列補(bǔ)償或重試操作，最終可以到達(dá)初始或者終止?fàn)顟B(tài)，且不會(huì)存在多條可能的事務(wù)執(zhí)行路徑最終所到達(dá)的終止?fàn)顟B(tài)間存在沖突。

考慮圖1所示的“秒殺購(gòu)物”場(chǎng)景。該服務(wù)組合包括填寫訂單（Fill_Order）、支付（Make_Payment）、預(yù)訂（PreOrder）、查找商品（Check_Item）、發(fā)貨（Ship_Order）這五個(gè)子事務(wù)，事務(wù)要求保證同一用戶僅能秒殺一次。在該組合流程中，用戶首先填寫訂單，接著進(jìn)入一個(gè)并發(fā)的流程，用戶可以進(jìn)一步立刻支付或選擇預(yù)訂，商家同時(shí)進(jìn)行查找商品和發(fā)貨操作，當(dāng)用戶和商家操作并行完成后，此訂單處理結(jié)束。這五個(gè)子事務(wù)中，支付服務(wù)由于其需要和外部支付代理交互，因此為不可補(bǔ)償也不可重試 （NC，NR），根據(jù)原子范圍定義，這一支付服務(wù)為關(guān)鍵（Pivot）子事務(wù)。發(fā)貨服務(wù)往往由于其成本原因一旦執(zhí)行就不可補(bǔ)償，因此其事務(wù)屬性為不可補(bǔ)償?shù)芍卦嚕∟C，R），預(yù)訂服務(wù)由于秒殺購(gòu)物的特殊性，一旦出現(xiàn)異常則只能補(bǔ)償，不可重試（C，NR），而其余參與服務(wù)的子事務(wù)都假設(shè)其事務(wù)屬性為可補(bǔ)償可重試（C，R）。在此服務(wù)組合中，存在3條可能的并發(fā)路徑：

①Fill_Order->Make_Payment

②Fill_Order->Pre-Order

③Fill_Order->Check_Item->Ship_Order

單純考慮此3條路徑，都滿足原子范圍中所定義的原子性。但若考慮并發(fā)流程時(shí)序上可能存在的交錯(cuò)性，對(duì)并發(fā)行為進(jìn)行組合后，在全局序列上將可能存Fill_Order->Check_Item->Ship_Order->Pre-Order，在此序列中Ship_Order這一僅可重試的服務(wù)在Pre-Order這一僅可進(jìn)行補(bǔ)償?shù)姆?wù)前發(fā)生，從而將導(dǎo)致原子范圍的違背和應(yīng)用不一致的發(fā)生。

另一方面，考慮兩操作者A，B以同一用戶ID在異地同步執(zhí)行此服務(wù)組合。若A執(zhí)行的最終流程為Fill_Order->Make_Payment->Check_Item->Ship_Order，B最終執(zhí)行的流程為Fill_Order->Pre-Order ->Check_Item->Ship_Order。由于A執(zhí)行流程中包括一個(gè)關(guān)鍵子事務(wù)Make_Payment而B不包括，則最終將導(dǎo)致出現(xiàn)同一用戶購(gòu)買了兩次，或者系統(tǒng)中對(duì)用戶是否支付的狀態(tài)上出現(xiàn)不一致的狀況。

從以上分析可知，在設(shè)計(jì)階段檢測(cè)服務(wù)組合事務(wù)一致性時(shí)，除考慮原子性的滿足外，還必須考慮其并發(fā)狀況下的時(shí)序組合及關(guān)鍵子事務(wù)所處位置。

22基于確定有限自動(dòng)機(jī)的Web服務(wù)組合建模

定義2.1Web服務(wù)組合的確定有限狀態(tài)自動(dòng)機(jī)（DFA）模型。Web服務(wù)組合的確定有限狀態(tài)自動(dòng)機(jī)模型可定義為一個(gè)五元組A=（Q，Σ，δ，q0，F(xiàn)）。其中，Q 是一個(gè)有限的狀態(tài)集合；ΣM表示請(qǐng)求一個(gè)組合中服務(wù)消息的有限集合，其中M為服務(wù)組合中的服務(wù)消息集合；δ：Q×∑→Q表示自動(dòng)機(jī)中的所有變遷；q0∈Q表示初始狀態(tài)；FQ代表終止?fàn)顟B(tài)的集合。

定義2.1中的模型是所有可能消息傳遞的組合結(jié)果，因此定義2.1中的模型事實(shí)上包含了當(dāng)前事務(wù)的所有可能執(zhí)行路徑。

文獻(xiàn)[17]對(duì)服務(wù)組合構(gòu)造自動(dòng)機(jī)模型的過程進(jìn)行了分析，本文首先利用上述文獻(xiàn)中的方法構(gòu)建一個(gè)僅包含基本的消息傳遞的有限狀態(tài)自動(dòng)機(jī)。圖2為圖1所示場(chǎng)景經(jīng)過轉(zhuǎn)換所得的確定有限狀態(tài)自動(dòng)機(jī)。

設(shè)定義2.1中服務(wù)組合的DFA模型拆分后的自動(dòng)機(jī)為Asplit 。我們將以Asplit作為服務(wù)組合一致性研究的基礎(chǔ)模型。

定義2.2完全狀態(tài)跡。對(duì)Asplit中的qn∈F，如果，σ1，σ2，...，σk∈∑，使得q0×σ1→q1，q1×σ2→q2，...，qk-1×σk→qn，則稱q0，q1，...，qn的序列為Asplit上的一個(gè)完全狀態(tài)跡ω，Asplit上的所有完全狀態(tài)跡的集合記為Trace（Asplit）。

由完全狀態(tài)跡定義可知，ω即代表Asplit上的一條事務(wù)執(zhí)行路徑。Trace（Asplit）為Asplit中所有可能的事務(wù)執(zhí)行路徑集合。考慮到事務(wù)一致性判定中需要基于同一事務(wù)執(zhí)行路徑同時(shí)刻畫正常執(zhí)行與異常執(zhí)行下的變遷，定義2.2采用狀態(tài)遷移序列替代了通常由變遷序列所定義的自動(dòng)機(jī)跡。在Asplit中由于任意兩個(gè)狀態(tài)間的遷移僅可能由唯一變遷引發(fā)，因此狀態(tài)序列將與變遷序列具備一一對(duì)應(yīng)關(guān)系。

圖2秒殺購(gòu)物場(chǎng)景服務(wù)組合確定有限自動(dòng)機(jī)模型

定義2.3部分跡。在Asplit在中，對(duì)q∈Q，q*代表從狀態(tài)q出發(fā)可能到達(dá)的狀態(tài)集，如果q，q1，...，qn∈q*，σ1，σ2，...，σk∈∑滿足q×σ1→q1，q1×σ2→q2，...，qk-1×σk→qn，則稱 q，q1，...，qn所組成的序列為q到qn的部分跡，記做μ（q，qn）。

23異常處理模型

由文獻(xiàn)[10]可知，每個(gè)服務(wù)變遷所對(duì)應(yīng)的子事務(wù)都有兩個(gè)正交的屬性：可補(bǔ)償性與可重試性。將兩正交屬性組合后，可得任一子事務(wù)其事務(wù)屬性取值集合為{（C，R），（C，NR），（NC，R），（NC，NR）}。endprint

定義2.4可補(bǔ)償變遷集SC。對(duì)σ∈∑，如果Comp（σ）=C則qσq′的變遷都屬于SC。其中Comp（σ）為獲得子事務(wù)可補(bǔ)償屬性的函數(shù)，其值域?yàn)閧C，NC}。

定義2.5可重試變遷集SR。對(duì)σ∈∑，如果Retry（σ）=R則qσq′的變遷都屬于SR。其中Retry（σ）為獲得子事務(wù)可補(bǔ)償屬性的函數(shù)，其值域?yàn)閧R，NR}。

定義2.6關(guān)鍵變遷集Spivot。對(duì)σ∈∑，如果Retry（σ）=NR∧Comp（σ）=NC則qσq′的變遷都屬于Spivot。

根據(jù)定義2.4-2.6，我們可在Asplit基礎(chǔ)上針對(duì)子事務(wù)的異常行為進(jìn)行建模。根據(jù)2.1節(jié)中事務(wù)概念一致性分析可知，需要對(duì)Asplit進(jìn)行補(bǔ)償與重試擴(kuò)展，擴(kuò)展規(guī)則為：

①對(duì)qσq′∈δ∧qσq′∈Sc ，δ=δ∪q′τcq；

②對(duì)qσq′∈δ∧qσq′∈Sr，δ=δ∪q′τrq.

因?yàn)樵贏split中我們已保證任意兩個(gè)狀態(tài)間僅可能由一個(gè)變遷引發(fā)，所以上述擴(kuò)展規(guī)則將具有唯一性，基于此擴(kuò)展后的δ可得：

定義2.7支持異常處理的擴(kuò)展有限狀態(tài)自動(dòng)機(jī)Aexec。Aexec也為五元組（Q，∑exec，δ，q0，F(xiàn)）：Q，δ，q0，F(xiàn)與定義2.1相同；∑execM∪{τc，τr}，其中M同定義2.1，{τc，τr}為異常行為變遷動(dòng)作，分別對(duì)應(yīng)補(bǔ)償動(dòng)作和重試動(dòng)作引發(fā)的變遷。

對(duì)于SC集合中的元素，都為可補(bǔ)償子事務(wù)，其異常處理方式為執(zhí)行補(bǔ)償任務(wù)并恢復(fù)到未執(zhí)行前的狀態(tài)。在Aexec中，所有τc補(bǔ)償動(dòng)作所引發(fā)的變遷集合為補(bǔ)償變遷集，其形式化的定義為：

定義2.8補(bǔ)償變遷集TRc。在Aexec中q∈Q，如果qτcq′∈δ，則qτcq′∈δ∈TRc。

類似的，SR集合中的元素，都為可重試子事務(wù)，其異常處理方式為不斷重試當(dāng)前動(dòng)作直到其成功變遷到下一狀態(tài)。在Aexec中，所有重試動(dòng)作所引發(fā)的變遷集合為重試變遷集，其形式化的定義為：

定義2.9重試變遷集TRr。在Aexec中q∈Q，如果q′τrq∈δ，則q′τrq∈δ∈TRr。

從文獻(xiàn)[14，18]對(duì)服務(wù)組合事務(wù)一致性分析可知，組合事務(wù)能否保持一致性僅和其異常處理動(dòng)作相關(guān)。事務(wù)發(fā)生異常時(shí)，若整個(gè)事務(wù)要保持一致性，則必然可通過若干重試變遷到達(dá)終止?fàn)顟B(tài)，或通過若干補(bǔ)償變遷到達(dá)初始狀態(tài)。結(jié)合定義2.6中的Aexec與TRc，TRr兩個(gè)變遷集合，可構(gòu)造出僅包含異常處理相關(guān)動(dòng)作和變遷的確定有限狀態(tài)自動(dòng)機(jī)。

定義2.10異常處理確定有限狀態(tài)自動(dòng)機(jī)Aexhandler。Aexhandler為五元組（Qcr，∑cr，δcr，q0，F(xiàn)cr）：q0同定義2.1；Fcr：F-f∈F∧fτcq′∈TRc∧q′τrf∈TRr；Qcr：Q-q∈Q∧qσq′∈TRr∪TRc∧q′σq∈TRr∪TRc；∑cr∈{τc，τr}；δcr∈TRr∪TRc.

Aexhandler模型，由于僅考慮異常處理相關(guān)變遷，其變遷集合為補(bǔ)償變遷集和重試變遷集的并集，其變遷動(dòng)作僅能為{τc，τr}中的一個(gè)。由Aexhandler構(gòu)造過程易知，對(duì)Asplit中的狀態(tài)集Q，如果q∈Q其事務(wù)屬性唯一確定，則Asplit所構(gòu)造的Aexhandler具備唯一性。

Aexhandler中終止?fàn)顟B(tài)集Fcr為Asplit中的終止?fàn)顟B(tài)集F去除所有孤立終止?fàn)顟B(tài)后所得。某終止?fàn)顟B(tài)為孤立終止?fàn)顟B(tài)當(dāng)且僅當(dāng)此狀態(tài)所有的前繼變遷都為關(guān)鍵子事務(wù)。在此情況下，該終止?fàn)顟B(tài)將緊隨關(guān)鍵子事務(wù)發(fā)生，進(jìn)行一致性判定時(shí)，僅需考慮關(guān)鍵子事務(wù)前所有狀態(tài)即可，所以將此類孤立終止?fàn)顟B(tài)從終止?fàn)顟B(tài)集中去除。

Aexhandler中的狀態(tài)空間Qcr為Asplit狀態(tài)空間去除所有孤立狀態(tài)所得。狀態(tài)為孤立狀態(tài)當(dāng)且僅當(dāng)其所有前繼和后續(xù)變遷均為關(guān)鍵子事務(wù)。此類狀態(tài)的出現(xiàn)意味著服務(wù)組合中出現(xiàn)了不止一個(gè)關(guān)鍵子事務(wù)，此種情況與事務(wù)原子范圍的原子性違背，所以對(duì)這類狀態(tài)的去除，同樣不影響一致性判定。

3Web服務(wù)組合一致性檢測(cè)

31服務(wù)組合一致性判定

定義3.1補(bǔ)償跡。在Aexhandler中，μ（q，qn）稱為q的補(bǔ)償跡，記做μcomp（q），當(dāng)且僅當(dāng)μ（q，qn）所代表狀態(tài)序列中任意兩個(gè)相鄰狀態(tài)之間的變遷都為τc。所有μcomp（q）的集合記為Tracecomp（q）。

定義3.2重試跡。在Aexhandler中，μ（q，qk）稱為q的補(bǔ)償跡，記做μretry（q），當(dāng)且僅當(dāng)qk∈q*∧qk∈Fcr使μ（q，qk）所代表狀態(tài)序列中任意兩個(gè)相鄰狀態(tài)之間的變遷都為τr。所有μretry（q）的集合記為Traceretry（q）。

由于在Asplit中已針對(duì)可能存在的并發(fā)時(shí)序交錯(cuò)建模，對(duì)Asplit進(jìn)行概念一致性判定時(shí)，我們僅需考慮如下兩個(gè)問題：

問題1：是否每個(gè)事務(wù)執(zhí)行路徑中的任意一個(gè)狀態(tài)出現(xiàn)異常時(shí)，事務(wù)都能保證放松的原子性；

問題2：整個(gè)事務(wù)中的關(guān)鍵子事務(wù)是否會(huì)導(dǎo)致最終事務(wù)出現(xiàn)多個(gè)不一致的最終狀態(tài)。

定理1（事務(wù)一致性判定定理）。對(duì)服務(wù)組合系統(tǒng)，若其對(duì)應(yīng)的Asplit可唯一構(gòu)造異常處理有限狀態(tài)自動(dòng)機(jī)Aexhandler，服務(wù)組合滿足事務(wù)一致性，當(dāng)且僅當(dāng)：

①在Asplit上，σ∈Σ∧qσq′∈ Spivot→（σ1∈∑∧σ≠σ1∧qσ1q′∈Spivot）

②在Asplit上，對(duì)σ∈Σ，如果qσq′∈Spivot，則對(duì) ω∈Trace（Asplit） →qi，qj∈ω∧qiσqj∈δ；

③對(duì)q∈Qcr，ω∈Trace（Asplit）如果q在ω 所代表的序列上，則在Aexhandler上有：（μ（q，q0）ω→μ（q，q0）∈Tracecomp（q））∨（（qn ∈Fcr∧μ（q，qn）ω）→μ（q，qn）∈）Traceretry（q））.endprint

3.2服務(wù)組合一致性判定實(shí)施框架

在第2章中，對(duì)服務(wù)組合及其異常處理進(jìn)行建模，在本節(jié)將討論服務(wù)組合的一致性判定的實(shí)施框架。圖 3 位服務(wù)組合一致性判定的實(shí)施框架。

結(jié)合第2章的分析，討論此實(shí)施框架的可行性。

Step1：流程的抽取

在此步驟中，服務(wù)設(shè)計(jì)者根據(jù)應(yīng)用規(guī)約完成服務(wù)組合流程設(shè)計(jì)。在實(shí)際應(yīng)用場(chǎng)景中，服務(wù)組合的建模方式具有多樣性（如UML活動(dòng)圖，BPEL，形式化描述等）。但任何一種建模方式，其最終模型都將包含：參與流程的服務(wù)、服務(wù)間交互行為以及流程的基本結(jié)構(gòu)這三個(gè)元素，從而使得根據(jù)這些組合模型轉(zhuǎn)變?yōu)楸疚闹械挠邢逘顟B(tài)自動(dòng)機(jī)模型成為可能。目前已有大量 Pi 演算、Petri 網(wǎng)、UML 活動(dòng)圖和 BPEL 等流程模型向自動(dòng)機(jī)模型轉(zhuǎn)換的相關(guān)研究，因此選取自動(dòng)機(jī)作為服務(wù)組合流程的描述，將不會(huì)成為實(shí)際實(shí)施的限制與障礙。

Step2：流程對(duì)應(yīng)的確定有限狀態(tài)自動(dòng)機(jī)的構(gòu)建

根據(jù)第2章分析易知，在此步驟中需要完成事務(wù)狀態(tài)空間分析，事務(wù)初始與終止?fàn)顟B(tài)設(shè)定，狀態(tài)之間遷移動(dòng)作分析并在此基礎(chǔ)上完成自動(dòng)機(jī)的構(gòu)建。這個(gè)過程可以由設(shè)計(jì)人員根據(jù)應(yīng)用規(guī)約手動(dòng)進(jìn)行，也可以根據(jù)第 1 步中的流程建模結(jié)果以及原始模型與有限狀態(tài)自動(dòng)機(jī)模型之間的轉(zhuǎn)換規(guī)則進(jìn)行自動(dòng)轉(zhuǎn)換得到。通過這樣方式構(gòu)建的有限狀態(tài)自動(dòng)機(jī)中將往往包含兩個(gè)狀態(tài)間存在不同遷移動(dòng)作的狀況，為后續(xù)的異常分析能夠進(jìn)行，還需要對(duì)此原始自動(dòng)機(jī)進(jìn)行狀態(tài)拆分，得到任意狀態(tài)轉(zhuǎn)變都僅由唯一遷移引發(fā)的Asplit模型。

Step3：事務(wù)相關(guān)屬性的獲取

事務(wù)屬性采用文獻(xiàn)[10]提出的可重試性與可補(bǔ)償性概念。對(duì)組合事務(wù)的每個(gè)子事務(wù)設(shè)定事務(wù)屬性時(shí)需要流程設(shè)計(jì)人員對(duì)全局事務(wù)的處理工作具有一定的了解，同時(shí)綜合考慮補(bǔ)償代價(jià)等因素進(jìn)行。本文與之前大量服務(wù)原子性與一致性相關(guān)研究一致，采納了任意子事務(wù)其事務(wù)屬性唯一確定的假定。但我們也注意到，實(shí)際應(yīng)用環(huán)境下，由于應(yīng)用的復(fù)雜性，服務(wù)本身可能具備不同狀態(tài)，同一服務(wù)在不同狀態(tài)下，將有可能具備不同的事務(wù)相關(guān)屬性。如對(duì)于銀行卡驗(yàn)證服務(wù)，當(dāng)用戶驗(yàn)證出錯(cuò)次數(shù)小于 3 次時(shí)，其可重試性為 R，但當(dāng)出錯(cuò)次數(shù)大于 3 時(shí)，其可重試性將為 NR。我們將在后續(xù)的研究中針對(duì)這一情況開展進(jìn)一步的分析。

Step4：定理 1 中條件 1，2 的檢測(cè)

針對(duì)定理 1 中的條件 1 和條件 2，需要判斷關(guān)鍵子事務(wù)出現(xiàn)次數(shù)和位置。因此直接在Asplit上進(jìn)行檢測(cè)。在實(shí)際實(shí)施過程中，這一步驟可以和步驟 5 同步進(jìn)行，我們將在下一節(jié)算法分析中對(duì)此進(jìn)行詳細(xì)的討論。

Step5：異常處理模型的構(gòu)造

根據(jù) 2.2 節(jié)的分析，完成此步驟首先需要根據(jù)步驟 3 中事務(wù)屬性在步驟 2 的結(jié)果上附加補(bǔ)償變遷與重試變遷。

Step6：約簡(jiǎn)模型上對(duì)定理 1 條件 3 的檢測(cè)，由于篇幅受限，本文并未介紹模型的約簡(jiǎn)過程。

在約簡(jiǎn)模型上的檢測(cè)可以得出一致性的最終判定結(jié)果。但我們也注意到，目前的檢測(cè)方式不方便業(yè)務(wù)人員快速定位一致性違背出現(xiàn)位置，這也將是我們的未來工作之一。

4結(jié)束語(yǔ)

Web服務(wù)組合中引入事務(wù)概念可以有效保障應(yīng)用一致性增強(qiáng)服務(wù)組合的可靠性，但傳統(tǒng)的數(shù)據(jù)庫(kù)事務(wù)的嚴(yán)格鎖定資源的方式不適合長(zhǎng)周期、松耦合的服務(wù)計(jì)算環(huán)境。異常處理方式放松了ACID的要求，通過柔性模型達(dá)到概念上的原子性與一致性，此時(shí)滿足放松原子性的事務(wù)，不再能保證同時(shí)滿足事務(wù)概念上一致性，需要對(duì)服務(wù)組合的一致性單獨(dú)進(jìn)行檢測(cè)。

本文基于確定有限狀態(tài)自動(dòng)機(jī)，對(duì)服務(wù)組合的交互以及異常處理進(jìn)行了建模，在此模型上進(jìn)一步提出了服務(wù)組合一致性的判定定理。最后針對(duì)整個(gè)檢測(cè)過程，分析了其實(shí)施框架及主要步驟。

本文的進(jìn)一步工作將包括對(duì)原始異常處理模型的約簡(jiǎn)，以及同時(shí)兼顧概念一致與應(yīng)用需求一致性的檢測(cè)以及在跨機(jī)構(gòu)環(huán)境下，基于等價(jià)替換與公開視圖的組合建模與一致性判定。

參考文獻(xiàn)

[1]PAPAZOGLOU M P，GEORGAKOPOULOS D.Service oriented computing[J].Communications of the ACM，2003，46（10）：2428.

[2]MUTANU L，KOTONYA G.ConsumerCentred Validation for Runtime Adaptation in ServiceOriented System[C]// IEEE，Conference on ServiceOriented Computing and Applications.IEEE Computer Society，2016：16-23.

[3]TSALGATIDOU A，PILIOURA T.An overview of standards and related technology in Web services[J].Distributed and Parallel Databases，2002，12（2-3）：135-162.

[4]QIAO X Q，WEI J，HUANG T.Service collaboration approach based on decentralized mediation model[J].Journal of Software，2009，20（6）：1470-1486.

[5]WIETRZYK V I，LAWSON R，TALIZAWA M，et al.Multimedia Distributed Infrastructure for B2B Operations in Web Services.[J].Ultraschall in Med，2016，4（01）：936-942.endprint

[6]GREENFIELD P，KUO D，NEPAL S，et al.Consistency for web services applications[C]//Proceedings of the 31st international conference on Very large data bases.VLDB Endowment，2005：1199-1203.

[7]PAPAZOGLOU M P，TRAVERSO P，DUSTDAR S，et al.Serviceoriented computing：A research roadmap[J].International Journal of Cooperative Information Systems，2008，17（02）：223-255.

[8]CASATI F，CUGOLA G.Error handling in process support systems[M]//Advances in exception handling techniques.Springer Berlin Heidelberg，2001：251-270.

[9]HASHMI K，MALIK Z，NAJMI E，et al.A Web Service Negotiation Management and QoS Dependency Modeling Framework[J].Acm Transactions on Management Information Systems，2016，7（2）：1-33.

[10]GARCIAMOLINA H，SALEM K.“SAGAS，”[J].SIGMOD Record，1987，16（3），249-259.

[11]GREFEN P，VONK J，APERS P.Global transaction support for workflow management systems：from formal specification to practical implementation[J].The VLDB JournalThe International Journal on Very Large Data Bases，2001，10（4）：316-333.

[12]LEEPA，ANDERSON T，F(xiàn)ault Tolerance：Principles and Practice，pp.143-185.SpringerVerlag，1990.

[13]HAGENC，ALONSO G.Exception Handling in Workflow Management Systems[J].IEEE Trans.Software Eng.，2000，26（10），943-958.

[14]YE C，CHEUNG S C，CHAN W K，et al.Atomicity analysis of service composition across organizations[J].IEEE Transactions on Software Engineering，2009，35（1）：2-28.

[15]REN Y，GUAN J，AO Q，et al.LHFR：A hierarchical failure recovery algorithm for long running transactions[J].Journal of Computer Research & Development，2010，47（10）：1805-1811.

[16]FISCHERJ，MAJUMDAR R.Ensuring Consistency in Long Running Transactions[J].Proc.22nd IEEE/ACM Intl Conf.Automated Software Eng.，2007，54-63.

[17]WOMBACHERA，F(xiàn)ANKHAUSER P，NEUHOLD E.Transforming BPEL into annotated deterministic_nite state automata for service discovery[C].In Proceedings of the 2nd IEEE International Conference on Web Services，pages 316{323，San Diego，CA，USA，July 2004.IEEE.

[18]SCHULDTH，ALONOSO G，BRRRI C，et al.Atomicity and Isolation for Transactional Processes[C].ACM Trans.Database Systems，2002，27（1），63-116.endprint