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