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

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.
5. De Michelis, G.., Ellis, C. & Memmi, G.., editors. (1994), Proceedings of the second Workshop on Computer-Supported Cooperative Work, Petri nets and related formalisms, Zaragoza, Spain.
6. Ellis, C.A. & Nutt, G.J. (1993), Modelling and Enactment of Workflow Systems, In M. Ajmone Marsan, editor, Application and Theory of Petri Nets 1993, volume 691 of Lecture Notes in Computer Science, 1-16. Berlin, Springer-Verlag.
7. Fu, X., Bultan, T., & Su, J. (2004), Analysis of Interacting BPEL Web Services, In Proceeding of the 13th International World Wide Web Conference, 621-630.
8. Fu, X., Bultan, T., & Su, J. (2004), Model Checking Interactions of Composite Web Services (Technical Report 2004-05), Computer Science Department, University of California at Santa Barbara.
9. Girault, C., & Valk, R. (2003), Petri Nets for Systems Engineering. A guide to modeling, Verification, and applications, New York, Springer.
10. Hamadi, R., & Benatallah, B. (2003), A Petri Net-based Model Web Service Composition, Fourteenth Australasian Database Conference (ADC2003), Adelaide, Australia. Conferences in Research and Practice in Information Technology, 191-200.
11. Holzmann, G. (2003), The Spin Model Checker, Addison-Wesley.
12. Huang, H., Tsai, W.T., Paul, R., & Chen, Y. (2005), Automated Model Checking and Testing for Composite Web Services, Proceedings of the eight IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC''05), 300-307.
13. International Business Machines Corporation, The IBM Business Process Execution Language for Web Services Java Run Time BPEL4J, Retrieved April 13, 2004, from http://www.alphaworks.ibm.com/tech/bpws4j.
14. Jensen, K. (1997), Coloured Petri Nets. Basic concepts, analysis methods and practical use (EATCS monographs on Theoretical Computer Science), Berlin, Springer-Verlag.
15. Jian, Y., & Mike, P. (2002), Web Component: A Substrate for Web Services Reuse and Composition, Proceedings of the 14th International Conference on Advanced Information System Engineering.
16. Milner, R. (1980), A Calculus of Communicating Systems, LNCS-92, Springer-Verlag.
17. Mitra, N, Simple Object Access Protocol (SOAP) Version 1.2. Retrieved June 24, 2003, from http://www.w3.org/TR/2003/REC-soap12-part0-20030624/.
18. Murata, T. (1989), Petri Nets: Properties, Analysis and Applications, Proceedings of the IEEE, 77(4), 541-580.
19. Narayanan, S., & Mcllraith, S. A. (2002), Simulation, Verification and Automated Composition of Web Services, Proceedings of the 11th international conference on World Wide Web, 77-88.
20. National Chiao Tung University, Intelligent Transportation Systems Project of Program for Promoting University Academic Excellence, from http://www.itstaiwan.org/.
21. Reisig, W. (1985), Petri nets: an introduction, volume 4 of Monographs in theoretical computer science : an EATCS series, Berlin, Springer-Verlag.
22. Russell, S., & Norvig, P. (2003), Artificial Intelligence A modern Approach, New Jersey, Prentice Hall.
23. Silva, M. & Valette, R. (1989), Petri Nets and Flexible Manufacturing (In G. Rozenberg, editor, Advances in Petri Nets, volume 424 of Lecture Notes in Computer Science), 274-417. Berlin, Springer-Verlag.
24. The Open Source BPEL Engine. ActiveBPEL Engine. Retrieved February 21 , 2006, from http://www.activebpel.org/.
25. Thomas, J.P., Thomas, M. & Ghinea, G. (2003), Modeling of Web Services Flow, Proceedings of the IEEE International Conference on E-Commerce (CEC’03), 391-398.
26. Tsai, W., Cao, Z., Chen, Y., & Paul, R. (2005), Web Services based Collaborative and Cooperative Computing, to appear in Workshop on Cooperative Computing, Internetworking, and Assurance Chengdu.
27. Tsai, W., Song, W., Paul, R., Cao, Z., & Hunag, H. (2004), Services-Oriented Dynamic Reconfiguration Framework for Dependable Distributed Computing, Proceedings of the 28th Annual International Computer Software and Applications Conference (COMPSAC''04), 554-559.
28. van der Aalst, W.M.P. (1999), Woflan: A Petri-net-based Workflow Analyzer, Systems Analysis - Modelling - Simulation, 35(3), 345-357.
29. van der Aalst, W.M.P. (1996), Three Good reasons for Using a Petri-net-based Workflow Management System, Proceedings of the International Working Conference on Information and Process Integration in Enterprises (IPIC''96), 179-201.
30. van Hee, K.M. (1994), Information System Engineering: a Formal Approach, Cambridge University Press.
31. van der Aalst, W.M.P. (2000), Workflow Verification: Finding Control-Flow Errors Using Petri-Net-Based Techniques, Lecture Notes In Computer Science; Vol. 1806 archive Business Process Management, Models, Techniques, and Empirical Studies, 161-183, London, Springer-Verlag.
32. Wohed, P., van der Aalst, W.M.P., Dumas, M. & ter Hofstede, A.H.M. (2002), Pattern-Based Analysis of BPEL4WS document, Technical Report FIT-TR-2002-04, QUT.
33. Wolf, M. & Reimer, U. (1996), editors. Proceedings of the International Conference on Practical Aspects of Knowledge Management (PAKM’96), Workshop on Adaptive Workflow, Basel, Switzerland.
34. Walton, C. (2004), Model Checking Multi-Agent Web Services, In Proceeding of AAAI Spring Symposium on Semantic Web Services.
35. Yi, X. & Kochut, K.J. (2004), A CP-nets-based Design and Verification Framework for Web Services Compositions, Proceedings of 2004 IEEE International Conference on Web Services, 756-760.