BPEL組合服務(wù)并發(fā)結(jié)構(gòu)的分析與驗(yàn)證.pdf

1、Web服務(wù)是一種新型的軟件泛型，它具備松耦合、高動(dòng)態(tài)性和可重配置等特點(diǎn)。Web服務(wù)組合通過(guò)為成員服務(wù)制定工作流程來(lái)實(shí)現(xiàn)具備復(fù)雜業(yè)務(wù)處理能力的組合服務(wù)，同時(shí)滿足了用戶不斷變化的需求。此外，Web服務(wù)依靠其良好的可復(fù)用性和靈活性等特征，加上服務(wù)組合可實(shí)現(xiàn)增值服務(wù)的能力，使得面向服務(wù)的計(jì)算成為一種具有里程碑意義的分布式計(jì)算技術(shù)。
　　 由于服務(wù)綱合為Web服務(wù)帶來(lái)了增值和復(fù)用的優(yōu)勢(shì)，如何對(duì)Web服務(wù)組合進(jìn)行建模、分析與驗(yàn)證，確保組合服

2、務(wù)的質(zhì)量與安全便成為一項(xiàng)值得深入研究的課題。現(xiàn)有的服務(wù)組合的驗(yàn)證方法一般從組合服務(wù)整體的狀態(tài)或各成員服務(wù)之間的消息交互方面出發(fā)進(jìn)行建模和分析；而本文則提出了一種擴(kuò)展的控制流圖(eXtended Control Flow Graph，XCFG)米對(duì)BPEL規(guī)范制定的組合服務(wù)工作流程進(jìn)行建模，定義了XCFG的形式化描述，并在此基礎(chǔ)上實(shí)現(xiàn)了BPEL中并發(fā)結(jié)構(gòu)相關(guān)的屬性：無(wú)死鎖性、無(wú)沖突性和link無(wú)冗余性的分析及驗(yàn)證。
　　 XCFG

3、針對(duì)傳統(tǒng)的控制流圖進(jìn)行了相應(yīng)的擴(kuò)展，使得其形式化模型能夠滿足對(duì)BPEL規(guī)范中提供的順序、選擇、并發(fā)和同步四種控制依賴關(guān)系進(jìn)行描述。此外，在XCFG的每個(gè)活動(dòng)節(jié)點(diǎn)元素中增加了對(duì)變量訪問(wèn)信息的記錄，用來(lái)實(shí)現(xiàn)并發(fā)訪問(wèn)沖突的分析。理論和實(shí)驗(yàn)分析表明，通過(guò)XCFG能夠有效的對(duì)BPEL規(guī)范制定的組合服務(wù)工作流程進(jìn)行控制流的建模、分析和驗(yàn)證。同時(shí)，以XCFG為基礎(chǔ)開(kāi)發(fā)的自動(dòng)化驗(yàn)證工具XCFGV4BPEL實(shí)現(xiàn)了從BPEL文檔解析生成相應(yīng)的BPEL對(duì)象模