一種基于接口自動機的BPEL4WS行為一致性的驗證及適配方法.pdf

1、隨著Web服務的出現(xiàn)和推廣，Web服務組合技術已經(jīng)成為近年來的研究熱點。Web服務的業(yè)務流程執(zhí)行語言(BPEL4WS)作為一種基于業(yè)務流程的服務組合方法，建模理論基礎比較薄弱，組合的正確性難以保證。因此業(yè)務流程的正確性、無死鎖性、行為一致性等問題，在它正式被實施前必須得到驗證。針對現(xiàn)有的BPEL4WS驗證方法使用的形式化方法較為復雜、不能以全面簡潔的方法直觀的表達需求規(guī)約、無法很好的滿足實際的應用需求等不足之處，本文在基于UML順序圖作

2、為需求規(guī)約的基礎上，提出了一種利用接口自動機對BPEL4WS的行為一致性進行驗證以及適配的方法。本文的主要工作包含以下幾個方面：
　　 1. 文章首先著重對BPEL4WS的行為一致性問題進行了分析，然后簡單的介紹了Web服務組合語言BPEL4WS和Web服務描述語言WSDL，闡述了BPEL4WS與WSDL兩者之間的關系，介紹了接口自動機的基本語法以及接口自動機在描述組件接口和組件組合方面的突出特點，最后分別給出了BPEL4WS與

3、WSDL 到接口自動機的轉換規(guī)則。
　　 2. 針對BPEL4WS的行為一致性分析與驗證問題，使用UML順序圖表示BPEL4WS的需求規(guī)約并將其投影為接口自動機的一個執(zhí)行片段，使用接口自動機及接口自動機網(wǎng)絡來描述BPEL4WS的行為設計模型，在此基礎上對BPEL4WS的應用實現(xiàn)與需求規(guī)約是否滿足行為一致性進行了分析與驗證并給出了相應的驗證方法。
　　 3.在對BPEL4WS 行為不一致的原因進行分析的基礎上，文章提出了一