BPEL組合服務并發(fā)結構的分析與驗證.pdf

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

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

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