複合式網際服務之塑模與驗證

網路服務組合在現今的服務導向架構中，逐漸扮演了重要的角色，早期的網路服務提供了功能讓需求者來使用，然而這些網路服務的功能往往無法符合需求者的需要。因此，網路服務組合讓需求者可依自身的需求把數個在網路上的網路服務串接成一個較大的網路服務，這種方式將帶來更大的附加價值以及更大的彈性。而運用工作流程來組合網路服務是目前最常見的方式，然而以流程來組合網路服務有很大的可能會因為流程設計上的錯誤而導致死結、潛在的無窮迴圈以及多餘的流程。這些問題將導致網路服務組合在執行時期時發生嚴重的錯誤。所以這些流程設計上的問題需要在網路服務組合執行之前進行驗證以確保流程設計是正確無誤的。本論文提出了以派翠網路為基礎的網路服務組合塑模與驗證方式。首先以派翠網路塑模網路服務組合，再利用Reachability，Coverability性質來分析派翠網路模型是否存在死結以及潛在的無窮迴圈，最後運用了深先搜尋演算法來得知網路服務組合中是否有多餘的流程。本論文的結果顯示，使用網路服務組合塑模及驗證方法可以確保網路服務組合流程的正確性並增加網路服務組合的可靠性。

關鍵字

塑膜；複合式網際服務；商業流程執行語言；派翠網路；驗證

並列摘要

In recent service-oriented architecture composite web services gradually play an important role. In earlier web service provides its capabilities in terms of functions in order to let service requester can make use of it. However these web services can not usually meet the need of service requester. The advantage of composite web services is to let service requester compose several web services according to the need of service requester. Thus, such a way brings value-added benefit and flexibility. Utilizing workflow to compose several web services is a common method at present. Nevertheless, utilizing workflow to compose several web services probably results in deadlock, potential infinite loop, and redundant flow because of flow design error. These problems will cause critical error of composite web services7 in design time. Therefore, there problems of flow design need to verify before executing composite web services. This thesis proposed modeling and verification of composite web services based on Petri nets. Firstly, after modeling workflow with Petri nets, I utilized properties of reachability, and coverability to analyze Petri net model in order to check whether deadlock and potential infinite loop exist in workflow. Lastly, I made use of depth-first search to examine whether redundant flow exists in workflow. This thesis showed that utilizing method of modeling and verification of composite web services can ensure correctness of flow of composite web services and enhance reliability of composite web services.

並列關鍵字

Composite Web Services ； Modeling ； Verification ； Petri nets ； BPEL4WS

參考文獻

1. BEA Systems, International Business Machines Corporation, Microsoft Corporation, SAP AG, & Siebel System. Business Process Execution Language for Web Services Version 1.1. Retrieved May 5, 2003, from http://www-128.ibm.com/developerworks/library/specification/ws-bpel/.

2. Booth, D., & Liu, C.K., Web Service Description Language (WSDL) 2.0. Retrieved March 27, 2006, from http://www.w3.org/TR/wsdl20-primer/.

3. Buhler, P., & Vidal, J. M. (2003), Towards Adaptive Workflow Enactment Using Multiagent Systems, Information Technology and Management Journal, 6(1), 61-87.

4. Cleaveland, R., & Sims, S. (1996), The NCSU concurrencyworkbench, In Proceedings of the 8th Conference on Computer Aided Verification, volume 1102 of Lecture Notes in Computer Science, 394-397.

11. Holzmann, G. (2003), The Spin Model Checker, Addison-Wesley.

國際替代計量

複合式網際服務之塑模與驗證

未授權

主題瀏覽