服務組合驗證的研究與實現(xiàn).pdf

1、隨著近年來服務計算和面向服務的架構(SOA)的迅速發(fā)展以及Web服務技術的成熟與完善，服務組合作為服務計算和SOA領域的核心問題已經越來越受到重視。WS-BPEL作為描述Web服務組合、編制和協(xié)調的語言，它提供了描述業(yè)務流程的豐富詞匯，從而利用服務組合實現(xiàn)新的服務功能。但是WS-BPEL卻缺乏對服務組合的正確性，有效性的驗證機制。這就造成了利用WS-BPEL描述的服務組合可能會存在系統(tǒng)風險，并可能造成重大損失。為此，本文提出了基于All

2、oy建模語言的服務組合驗證方案。
　　 本文的研究工作可以總結為以下幾個部分：
　　 1.介紹了服務計算目前的發(fā)展情況，總結了服務計算領域服務組合的方法，并且根據目前服務組合驗證領域的研究現(xiàn)狀，完整總結了目前服務組合驗證使用的四種方法和其中使用的技術。
　　 2.提出了基于Alloy的服務組合驗證方案，該方案利用Alloy描述服務組合，得到Alloy模型，然后根據系統(tǒng)需求將系統(tǒng)屬性進行轉換得到Alloy約束，最后

3、兩者作為Alloy Analyzer的輸入用于服務組合的分析。這種方案綜合了嚴謹性，增量性和可視化的優(yōu)點，提供了完整、有效的分析方案。
　　 3.本文提出了使用有限狀態(tài)機來建模服務組合，描述系統(tǒng)的狀態(tài)變化，并詳細介紹了從WS-BPEL到Alloy的轉換方法。使用有限狀態(tài)機作為中間表示，方便了從WS-BPEL到Alloy的轉換。接著，本文總結了使用Alloy Analyzer分析Alloy模型的理論基礎——滿足性理論和前提假設——