服務(wù)組合驗(yàn)證的研究與實(shí)現(xiàn).pdf

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

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

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