異步Web服務組合分析與驗證方法研究.pdf

1、隨著網(wǎng)絡技術(shù)的迅速發(fā)展，面向服務的體系架構(gòu)(SOA)以其良好的可重用性、松耦合性和互操作性，已成為一種工業(yè)界和學術(shù)界廣泛接受的網(wǎng)絡化軟件應用模式。Web服務作為SOA的主流實現(xiàn)方式，正逐步成為網(wǎng)絡環(huán)境中資源封裝的標準方式。目前，Web服務正逐步由單一的面向功能向面向業(yè)務流程轉(zhuǎn)變，服務周期隨之延長，使得同步通信模式的Web服務已無法滿足用戶需求，而無阻塞的異步Web服務成為研究熱點。
　　 由于單個的Web服務提供的功能有限，為了

2、更加充分地利用共享的Web服務構(gòu)建企業(yè)級應用系統(tǒng)，Web服務組合技術(shù)變得愈加重要。Web服務組合研究領(lǐng)域的一個重要的問題是如何形式化描述Web服務組合以及如何驗證服務組合的正確性。在對Web服務組合的模型進行驗證時，不僅要考慮組合服務是否滿足功能需求，還需要檢查是否存在時間沖突或數(shù)據(jù)不一致等問題，確保構(gòu)建高效正確的服務組合。
　　 本文以異步Web服務為研究對象，分析相關(guān)時間和數(shù)據(jù)約束對服務交互的影響，對異步Web服務組合驗證進

3、行了深入研究。主要內(nèi)容包括：(1)從軟件體系結(jié)構(gòu)的角度研究Web服務組合，分析基于時序邏輯的軟件體系結(jié)構(gòu)描述語言XYZ/ADL在描述Web服務組合方面的優(yōu)勢，采用XYZ/ADL來描述服務組合的交互行為，相關(guān)的時間和數(shù)據(jù)約束用XYZ/RE表示。(2)基于有限狀態(tài)自動機理論，建立異步Web服務的形式化模型。針對僅涉及時間約束的Web服務建立時間異步通信模型(TACM)，該模型符合UPPAAL規(guī)約，用消息隊列模擬異步通信，用時間自動機中的標準