一種基于接口自動(dòng)機(jī)的BPEL4WS行為一致性的驗(yàn)證及適配方法.pdf

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

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

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