基于PI-演算的CPN在移动通信服务建模的研究与应用
|
摘要
随着业务要求的不断增加,Web服务组合变得日益复杂,服务组合出错的可能性也不断增加,这就需要对Web服务组合流程进行分析和验证,以保证服务组合的正确性和可靠性。
本文的主要研究内容包括:(1)提出了一个基于有色Petri网(Colored Petri Nets,CPN)的Web服务组合模型;(2)基于该组合模型,给出了编排规则生成算法;(3)说明了如何将BPEL4WS转换为CPN模型,设计了一个可视化的分析验证工具JCPN;(4)提出用PI-演算把通信过程封装成多个Web Service,并来描述这些Web Service及服务组合,使每个通信过程的实现都是调用相关Web Service或Web Service组合;(5)概括总结了PI-演算互模拟的相关定义,使用MWB工具对移动通信模型中的PI-演算表达式进行语法分析和验证;(6)为弥补PI-演算的固有缺陷,提出一种将PI-演算映射为CPN的规则,将移动通信中的PI-演算模型映射为Petri网,验证了方法的有效性。
Web Services composition is the ability to create a new value-added service by incorporating some existing Web Services together. Web Services composition is usually an error-prone task, and repairing errors at services operation time is usually costly. Web Services participated in composition are often with complex operations, and these operations must be invoked according to the precisely defined scheduling rules, so it’s necessary to define the choreography rules for the operations. But some existing Web Services composition languages only describe how to compose many elementary services into a composite service in syntax, but lack formal semantic, so it is difficult to analyze and verify these models built by these languages. These languages have not provided the techniques for choreographing complex operations either, and are unable to model concurrency and communication, so they are not suitable to define the choreography rules for Web Services. Formal model can solve these problems. Creating formal model for Web Services composition process can use formal techniques to analyze and verify the services composition process in order to ensure the correctness and reliability of the composition. Formal model also can define services choreography rules. This approach enables designers to test and repair design errors even before actual running of the service, or allow designers to detect erroneous properties and formally verify whether the service process design does have certain desired properties. The main contents and conclusions in this dissertation can be summarized as follows:
Ⅰ. Study on Web Services Composition Based on Colored Petri Nets
1. This paper proposes a CPN-based model for Web Services composition, which is capable to specify choreography rules and Web Services composition. By creating CPN model for services composition process, designers can use the formal semantic and analysis techniques of CPN to detect and repair the design errors as early as possible at design stage, thus ensure the correctness of the composition. Choreography rules define the invoking rules of WSDL operations and describe the external behaviors. Defining services choreography rules can ensure the services to be invoked correctly and allow the composition involving services with complex operations.
2. Based on the Web Services composition model, this paper presents choreography rules derivation algorithm. The basic idea of the derivation algorithm is simplifying the WSCNet service composition model, while preserving its externally observable interaction behavior. Choreography rules derivation algorithm is based on CPN full occurrence graph construction. With the use of this algorithm, choreography rules can be derivated automatically from the CPN-based model for Web Services composition, and the choreography rules will be published with its WSDL interface to UDDI registry. The Web Services composition is exposed as a new Web Service for other users, and other users can use this new service conveniently, which will improve the reuse of the service.
3. This paper gives the translation between BPEL4WS and CPN model. In BPEL4WS, both the Web Service composition and the choreography rules are specified as workflows consisting of activities. To represent BPEL4WS using CPN, basically we represent activities with CPN transitions. The control flow relations between activities specified in BPEL4WS are captured by CPN token firing rules. This paper considers the mostly used workflow patterns in BPEL4WS and discuss how to represent them using CPN model.
4. This paper presents the steps of creating Web Services composition using the Web Services composition model. There are five steps: (1)discover component services and acquire their service descriptions including both WSDL interface and choreography rules; (2)describe the composite Service; (3)construct the Web Service composition from CPN to BPEL4WS; (4)derive choreography rules of the composite service; (5)deploy and advertise the composite service.
5. In order to ensure the correctness of the Web Services composition model, it’s necessary to analyze and verify the model. This paper gives the approach for analyzing and verifying the model, and designs an analysis and verification tools JCPN. JCPN can be used to detect deadlocks automatically and has also been applied intensively in the specification, design and analysis of service-oriented distributed systems. This paper designs several examples to test the functionalities of JCPN.
Ⅱ. Study on mobile communication service based on PI-calculus and Application
1. There are too many problems in mobile communication system now, so the paper proposes that we should improve mobile communication service with the thought of Web Service. Mainly Internet as a develoPIng platform, and encapsulate many Web Service with communication process, and describe these Web Services and Web Services composition by PI-calculus, so implementing every communication process by invoking Web Service or Web Service composition. Give out four examples, in order to explain how to model Web Service by PI-calculus in mobile communication process. They are: modeling mobile communication initialization connection process, modeling mobile communication process, modeling mobile communication base station switching process, modeling recalling process. Describe Web Service composition by PI-calculus, and discuss how to describe dynamic changeable service, and abstract concrete PI-calculus expression.
2. In the research of mobile process calculus, process equivalence is a core problem all the time: it means when two process expression with different syntax formations are behavior equivalence. The paper summarizes some definitions about PI-calculus bisimulation. In the process calculus, popular equivalence relation as follow: bisimulation equivalence, test equivalence, trace equivalence and so on, and bisimulation equivalence is most influential of all.
3. In order to remedy the deficiencies of PI-calculus, PI-calculus is mapped into Petri nets. PI-calculus is divided into the basic elements, sequence, concurrency, choices and recursive modules. These modules are mapped into Petri nets respectively, which const ruct a complicated system. Petri nets semantics for PI-calculus visually describe system structure as well as system behaviors, and the qualitative analysis of properties is proved directly on the st ructure of the nets.
With the development of Web Services composition and myriads of changes on various business in mobile communication network, data fusion and business reorganization will become more and more important and contribute more to the future various industries. The results of the dissertation will contribute to the study on formal research of modeling Web Services composition based on PI-calculus and mobile communication business based on Web Services.
本文的主要研究内容包括:(1)提出了一个基于有色Petri网(Colored Petri Nets,CPN)的Web服务组合模型;(2)基于该组合模型,给出了编排规则生成算法;(3)说明了如何将BPEL4WS转换为CPN模型,设计了一个可视化的分析验证工具JCPN;(4)提出用PI-演算把通信过程封装成多个Web Service,并来描述这些Web Service及服务组合,使每个通信过程的实现都是调用相关Web Service或Web Service组合;(5)概括总结了PI-演算互模拟的相关定义,使用MWB工具对移动通信模型中的PI-演算表达式进行语法分析和验证;(6)为弥补PI-演算的固有缺陷,提出一种将PI-演算映射为CPN的规则,将移动通信中的PI-演算模型映射为Petri网,验证了方法的有效性。
Web Services composition is the ability to create a new value-added service by incorporating some existing Web Services together. Web Services composition is usually an error-prone task, and repairing errors at services operation time is usually costly. Web Services participated in composition are often with complex operations, and these operations must be invoked according to the precisely defined scheduling rules, so it’s necessary to define the choreography rules for the operations. But some existing Web Services composition languages only describe how to compose many elementary services into a composite service in syntax, but lack formal semantic, so it is difficult to analyze and verify these models built by these languages. These languages have not provided the techniques for choreographing complex operations either, and are unable to model concurrency and communication, so they are not suitable to define the choreography rules for Web Services. Formal model can solve these problems. Creating formal model for Web Services composition process can use formal techniques to analyze and verify the services composition process in order to ensure the correctness and reliability of the composition. Formal model also can define services choreography rules. This approach enables designers to test and repair design errors even before actual running of the service, or allow designers to detect erroneous properties and formally verify whether the service process design does have certain desired properties. The main contents and conclusions in this dissertation can be summarized as follows:
Ⅰ. Study on Web Services Composition Based on Colored Petri Nets
1. This paper proposes a CPN-based model for Web Services composition, which is capable to specify choreography rules and Web Services composition. By creating CPN model for services composition process, designers can use the formal semantic and analysis techniques of CPN to detect and repair the design errors as early as possible at design stage, thus ensure the correctness of the composition. Choreography rules define the invoking rules of WSDL operations and describe the external behaviors. Defining services choreography rules can ensure the services to be invoked correctly and allow the composition involving services with complex operations.
2. Based on the Web Services composition model, this paper presents choreography rules derivation algorithm. The basic idea of the derivation algorithm is simplifying the WSCNet service composition model, while preserving its externally observable interaction behavior. Choreography rules derivation algorithm is based on CPN full occurrence graph construction. With the use of this algorithm, choreography rules can be derivated automatically from the CPN-based model for Web Services composition, and the choreography rules will be published with its WSDL interface to UDDI registry. The Web Services composition is exposed as a new Web Service for other users, and other users can use this new service conveniently, which will improve the reuse of the service.
3. This paper gives the translation between BPEL4WS and CPN model. In BPEL4WS, both the Web Service composition and the choreography rules are specified as workflows consisting of activities. To represent BPEL4WS using CPN, basically we represent activities with CPN transitions. The control flow relations between activities specified in BPEL4WS are captured by CPN token firing rules. This paper considers the mostly used workflow patterns in BPEL4WS and discuss how to represent them using CPN model.
4. This paper presents the steps of creating Web Services composition using the Web Services composition model. There are five steps: (1)discover component services and acquire their service descriptions including both WSDL interface and choreography rules; (2)describe the composite Service; (3)construct the Web Service composition from CPN to BPEL4WS; (4)derive choreography rules of the composite service; (5)deploy and advertise the composite service.
5. In order to ensure the correctness of the Web Services composition model, it’s necessary to analyze and verify the model. This paper gives the approach for analyzing and verifying the model, and designs an analysis and verification tools JCPN. JCPN can be used to detect deadlocks automatically and has also been applied intensively in the specification, design and analysis of service-oriented distributed systems. This paper designs several examples to test the functionalities of JCPN.
Ⅱ. Study on mobile communication service based on PI-calculus and Application
1. There are too many problems in mobile communication system now, so the paper proposes that we should improve mobile communication service with the thought of Web Service. Mainly Internet as a develoPIng platform, and encapsulate many Web Service with communication process, and describe these Web Services and Web Services composition by PI-calculus, so implementing every communication process by invoking Web Service or Web Service composition. Give out four examples, in order to explain how to model Web Service by PI-calculus in mobile communication process. They are: modeling mobile communication initialization connection process, modeling mobile communication process, modeling mobile communication base station switching process, modeling recalling process. Describe Web Service composition by PI-calculus, and discuss how to describe dynamic changeable service, and abstract concrete PI-calculus expression.
2. In the research of mobile process calculus, process equivalence is a core problem all the time: it means when two process expression with different syntax formations are behavior equivalence. The paper summarizes some definitions about PI-calculus bisimulation. In the process calculus, popular equivalence relation as follow: bisimulation equivalence, test equivalence, trace equivalence and so on, and bisimulation equivalence is most influential of all.
3. In order to remedy the deficiencies of PI-calculus, PI-calculus is mapped into Petri nets. PI-calculus is divided into the basic elements, sequence, concurrency, choices and recursive modules. These modules are mapped into Petri nets respectively, which const ruct a complicated system. Petri nets semantics for PI-calculus visually describe system structure as well as system behaviors, and the qualitative analysis of properties is proved directly on the st ructure of the nets.
With the development of Web Services composition and myriads of changes on various business in mobile communication network, data fusion and business reorganization will become more and more important and contribute more to the future various industries. The results of the dissertation will contribute to the study on formal research of modeling Web Services composition based on PI-calculus and mobile communication business based on Web Services.
引文
[1] Nanda MG, Karnik N. Synchronization Analysis for Decentralizing Composite Web Services[J], International Journal of Cooperative Information systems, 2004, 13(1): 91-119.
[2]葛声,马殿富,胡春明等.基于Web服务的网络软件运行平台研究与实现[J],北京航空航天大学学报,2003, 29(10): 897-900.
[3] F. Casati, S. Ilnicki, L.J. Jin, et al. eflow :A Platform for Developing and Managing Composite e-Services. Academia-Industry Working Conference on Research Challenges. IEEE Computer Society, April 27-29, 2000[C]. USA, Buffalo Press, 2000.
[4] Boualem Benatallah, Quan Z. Sheng, Marlon Dumas. The Self-Serv Environment for Web Services Composition[J]. IEEE Internet Computing, 2003,7(1):40-48.
[5] Abhijit Patil, Swapna Oundhakar, Amit Sheth, et al. METEOR-S Web Service Annotation Framework[C]. The 13th International World Wide Web Conference, New York, USA: 533-562.
[6] Ponnekanti SR, Fox A. SWORD: A developer Toolkit for Web Service Composition[C]. In: Proc. of the Int'l World Wide Web Conf. Honolulu, 2002. 83-107
[7] B.Holtkamp, R.Gartmann, Y.Han. FLAME2008--Personalized Web Services for the Olympic Games 2008 in Beijing[C]. in Proc. eChallenges, e-2003, 2003.
[8] Erik Christensen, F.C., Greg Meredith, et al. Web Services Description Language (WSDL)1.1[R]. W3C. 2001.
[9] Martin Gudgin, M. H, SOAP Version 1.2 Part 1: Messaging Framework (Second Edition), [R]. W3C. 2007.
[10] Luc Clement, A. H., Claus von Riegen, et al. UDDI Version 3.0.2[R]. UDDI Spec Technical Committee Draft, [2004-10-19].
[11] S. Thatte. XLANG Web Services for Business Process Design[R]. OASIS. [2001-06-06].
[12] Frank Leymann. Web Services Flow Language (WSFL) 1.0[R]. IBM Software Group. 2001.
[13] A. Arkin. Business Process Modeling Language (BPML)1.0[R]. OASIS. 2003.
[14] A. Arkin, Scott Fordin,Wolfgang Jekeli. Web Service Choreography Interface (WSCI)1.0[R]. W3C. 2002.
[15] DAML Joint Committee. Daml Services (Daml-S)[R]. http://www.daml.org/services /owl-s/. 2003.
[16] D. Martin. OWL-S1.1[R]. http://www.daml.org/services/owl-s/l.1/. 2004.
[17] DAML Joint Committee. Daml+oil language[R]. http://www.daml.org/2001/03/ daml+oil-index.html. 2001.
[18] N. Kavantzas, D.Burdett. Web Services Choreography Description Language (WS-CDL) 1.0[R]. http://www.w3c.org/TR/ ws-cdl-10/. 2005.
[19] T.Andrews, F.Curbera, H.Dholakia, et al. Business Process Execution Language for Web Services (BPEL4WS) version 1.1[R]. http://xml.coverpages.org/bpel4ws.html. 2003.
[20] C.Yushi, L.E.Wah, D.K.Limbu. Web Services Composition- An Overview of Standards [J]. Synthesis Journal. 2005:137-150.
[21]吕庆中,韩燕波,麦中凡. Web服务环境中的业务过程建模语言比较框架.计算机工程与应用. 2003,23:7-13.
[22] Mendling, J., Müller, M., A Comparison of BPML and BPEL4WS, In: proceedings of the 1st Conference "Berliner XML-Tage", 2003, pages305-316.
[23] W.M.P., van der Aalst, etc. Web Service Composition Languages: Old Wine in New Bottles 29th EUROMICRO Conference: New Waves in System Architecture, 2003, pages 298-305.
[24] P. Wohed, W. M. P. v. d. A., M. Dumas, A.H.M ter Hofstede (2002). Pattern-Based Analysis of BPEL4WS.
[25] J. Rao and X. Su, A Survey of Automated Web Service Composition Methods, In: proceedings of the First International Workshop on Semantic Web Services and Web Process Composition, 2004.
[26] B. Srivastava and J. Koehler, Web Service Composition - Current Solutions and Open Problems, The 13th International Conference on Automated Planning & Scheduling (ICAPS), Italy, 2003.
[27] N. Milanovic and M. Malek, Current Solutions for Web Service Composition, Published by the IEEE Computer Society, 2004, www.informatik.hu-berlin.de/~milanovi/wscomp-survey-milanovic.pdf
[28] S. Majithia, M. Shields, etc., Triana: A Graphical Web Service Composition andExecution Toolkit, International Conference on Web Services, 2004.
[29] Cardoso, A. Sheth, Semantic e-Workflow Composition, Journal of Intelligent Information systems, 2003.
[30] D. Shuiguang, Managing Service flow in a Flexible, The 5th International Conference on Web Information Systems Engineering, 2004.
[31] S. Chadrasekaran, J. A. Miller, Composition, Performance Analysis and Simulation of Web Services, The International Journal of Electronic Commerce and Business Media, 2003.
[32] H. Yanbo, Z. Zhuofeng, etc., CAFISE: An Approach to Enabling Adaptive Configuration of Service Grid Applications, Journal of Computer Science and Technology, 2003.
[33] Sheila McIlraith, Tran Cao Son, Adapting Golog for Composition of Semantic Web Services, In: proceedings of the 8th International Conference on Knowledge Representation and Reasoning, 2002.
[34] W. M. P. Van Der Aalst, A. A. H. M. T. H., A. B. Kiepuszewski, Workflow Patterns, istributed Parallel Databases 14 (1), 2003.
[35] Evren Sirin, .etc, HTN Planning for Web Service Composition Using SHOP2, http://www.mindswap.org/papers/SHOP2JWS.
[36] J. Billington, S. Christensen, .etc, The Petri Net Markup Language: Concepts, Technology, and Tools. ICATPN 2003: 483-505.
[37] Arindam Banerji, .etc, (2002). Web Services Conversation Language (WSCL) 1.0. http://www.w3.org/TR/2002/NOTE-wscl10- 20020314/.
[38] Brahim Medjahed, Athman Bouguettaya, etc, Composing Web Services on the semantic web, The VLDB Journal, 2003, 12(4).
[39] Design/CPN, http://www.daimi.au.dk/designCPN/
[40] AT&T, Graphviz - Graph Visualization Software, 2005.
[41] Apache, X, The Document Object Model, 2005.
[42] X. Fu, T. Bultan and J. Su, Analysis of interacting BPEL Web Services, In: proceedings of the 13th International World Wide Web Conference, May 2004. ACM, pages 621-630.
[43] X. Fu, T. Bultan and J. Su, Synchronizability of conversations among Web Services, IEEE Transactions on Software Engineering, 31 December, 2005, (12):1042-1055.
[44] CPN tools. http://www.daimi.au.dk/CPNtools/
[45] D. Fahland and W. Reisig, ASM-based semantics for BPEL: The negative control flow, In proceedings of the 12th International Workshop on Abstract State Machines, 2005, pages 131-151.
[46]郭玉彬,杜玉越,奚建清,Web服务组合的有色网模型及运算性质,计算机学报,2006年第29卷07期.
[47] W. Reisig, Modeling and analysis techniques for Web Services and business processes, In: proceedings of the 7th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, 2005,vol.3535, pages 243-258.
[48] K. Jensen, Colored Petri Nets Basic Concepts, Analysis Methods and Practical Use, Volume 1, second edition, 1996.
[49] R. Kazhamiakin and M. PIstore, Parametric communication model for the verification of BPEL4WS compositions, In: Proceedings of the 2nd International Workshop on Web Services and Formal Methods, volume 3670 of Lecture Notes in Computer Science, 2005, pages 318-332.
[50] Hamadi R, Benatallah B, A Petri Net-Based Model for Web Service Composition, In: 4th Australasian Database Conf. (ADC2003), Adelaide, Australia, Conferences in Research and Practice in Information Technology, 2003, Vol.17.
[51] Zhang Jia, Chung Jen-Yao, Chang C. K., Kim S., WS-Net: A petri-net based specification model for Web Services, In: Proceedings of the 2nd IEEE International Conference on Web Servies, USA, 2004, 420-427.
[52] H. Foster, S. Uchitel, J. Magee and J. Kramer, Model-based Verification of Web Service Compositions, In: Proceedings of the 18th IEEE International Conference on Automated Software Engineering Conference (ASE 2003), 2003.
[53] Karamanolis C., Giannakopoulou D., Magee J., Wheater S. M, Model Checking of Workflow Schemas, Proc. of 4th IEEE/OMG International Enterprise Distributed Object Computing Conference (EDOC), 2000.
[54] H. Foster, S. Uchitel, J. Magee and J. Kramer, Compatibility for Web Service Choreography, presented at 3rd IEEE International Conference on Web Services (ICWS), San Diego, CA, 2004.
[55] Ferrara A, Web Services: A process algebra approach, In: Proceedings of the 2nd International Conference on Service Oriented Computing, 2004, pages 242-251.
[56]廖军,谭浩,刘锦德,基于PI-演算的Web服务组合的描述和验证,计算机学报,2005,28(4):635-642.
[57] Salaun G, Bordeaux L, Schaerf M, Describing and reasoning on Web Services using process algebra, In: Proceedings of the 2nd IEEE International Conference on Web Services, 2004, pages 43-51.
[58] A. Wombacher, P. Fankhauser and E. Neuhold, Transforming BPEL into annotated deterministic finite state automata for service discovery, In: Proceedings of the 2nd IEEE International Conference on Web Services, San Diego, CA, USA, July 2004, IEEE, pages 316-323.
[59]袁崇义,Petri网原理与应用.电子工业出版社,2005.
[60] Business Process Management Initiative,Business Process Modeling Language v1.0,2002,http://www.bpmi.org [61 Hamadi R,Benatallah B,A Petri Net-based Model for Web Services Composition,Proc. of the Fourteenth Australasian Database Conference on Database Technologies,2003
[62]郭小群,郝克刚,Web服务的PI-演算描述,计算机科学,Vol.33,No.3,2006
[63] Biplay S,Jana K,Web Services Compositon-Current Solution and Open Problems, http://www.zurich.ibm.com/pdf/ebizz/icaps-ws.pdf
[64] Web服务的业务流程执行语言版本1.1,2003年5月5日
[65] Tadao Murata,Petri Net: Properties、Analysis and Applications, Proceedings of the IEEE,1989,77(4):541-580
[66] Milner R,Communication and Concurrency,Englewood Cliffs:Prentice-Hall,1989
[67] Fensel D,The semantic Web and its languages,IEEE Intelligent Systems,2000,15(6):67-73
[68] Milner R,Communication and Mobile Systems:The PI-Calculus, Cambridge University Press,1999
[69] Milner R,Parrow J,Walker D,A calculus of mobile processes, part I/II,Journal of Information and Computation,1992,100(1):1-77
[70] Lin Hui-Min,Complete proof systems for observation congruences in finite control PI-calculus,Proceedings of the 25th International Colloquium on Automata,Languages and Programming,Aalborg,Denmark,1998,442-450
[71] Jiao Wen-PIn,Zhou Ming-Hui,Wang Qian-Xiang,Formal framework for adaptivemulti-agent Systems,Proceedings of IEEE/WIC International Conference on Intelligent Agent Technology,Halifax,Canada,2003
[72] Makus Lumpe,A PI-calculus based approach to software composition,Institute of Computer Science and Applied Mathematics,University of Bern,Switzerland,1999
[73] Bjorn Victor,The Mobility Workbench User’s Guide Polyadic version 3.122,1994
[74] Bjorn Victor,Faron Moller. The Mobility Workbench-A Tool for the PI-Calculus,1994
[75] Bjorn Victor,A Verification Tool for the Polyadic PI-Calculus. May 9,1994
[76]李东来,王丰锦,韩燕波,基于Web服务的动态工作流系统中资源管理问题,计算机工程,Vol.29,No.18,2003年10月
[77]石静,丁长明,赵泽宇,薛向阳,Web服务合成研究综述,计算机科学,vol.31,No.6,2004
[78] Benatallah B,Dumas M,Declarative Compositon and Peer-to-Peer Provisioning of Dynamic Web Services, Proc.of the 18th Intl.conf,Data Engineering(ICDE.02),IEEE Computer Society,2002
[79] Chakraborty D,Joshi A,Dynamic Service Compositon: State-of-the-Art and Research Directions:[Technical Report TR-CS-01-19]UMBC,December,2001, http://research.ebiquity.org/re/papers.html
[80] Benjamin C.PIerce,Programming in the PI-Calculus,Department of Computer Science University of Edinburgh
[81] Robin Milner,The Polyadic PI-Calculus:a Tutorial,Laboratory for Foundations of Computer Science,Computer Science Department,University of Edinburgh,The King’s Buildings Edinburgh EH9 3JZ,UK,October,1991
[82] Fredrick B.Beste,The Model Prover-a sequent-calculus based modal PI-calculus model checker tool for finite control PI-calculus agents,1998.1.9
[83] Gian Luca Cattani,Ian Stark and Glynn Winskel,Presheaf Models for the PI-Calculus,BRICS,Department of Computer Science,University of Aarhus,Denmark,December,1997
[84] Lucian WIschik,New directions in implementing the PI-calculus,University of Bologna,30th,August,2002
[85] T.Andrews,F.Curbera,H.Dholakia,Y.Goland,J.Klein,F.Leymann,K.Liu,D.Roller,D.Smith,S.Thatte,I.Trickovic,and S.Weerawarana,Business Process execution language for WebServices,version1.1, http://www-128.ibm.com/developerworks/webservices/library/ws-bpel/index.html, 2003.5
[86] Nickolas Kavantzas.etal,Web Services Choreography Description Language Version 1.0,2004
[87] Orava F,Parrow J,An algebraic verification of a mobile network,Formal Aspect of Computing,1992,4(6)
[88]廖军,谭浩,刘锦德,基于PI-演算的Web服务可替换性验证,华中科技大学学报(自然科学版)Vol.33, 2005.12
[89] Riccardo Pucella,Notes on Programming Standard ML of New Jersey(version 110.0.6), 2001, http://www.cs.cornell.edu/riccardo/prog-smlnj/notes-011001.pdf
[90] Raymond Devillers,Hanna Klaudel,Maciej Koutny,Petri net semantics of the finite PI-calculus,School of Computing Science,University of Newcastle upon Tyne,June 2004
[2]葛声,马殿富,胡春明等.基于Web服务的网络软件运行平台研究与实现[J],北京航空航天大学学报,2003, 29(10): 897-900.
[3] F. Casati, S. Ilnicki, L.J. Jin, et al. eflow :A Platform for Developing and Managing Composite e-Services. Academia-Industry Working Conference on Research Challenges. IEEE Computer Society, April 27-29, 2000[C]. USA, Buffalo Press, 2000.
[4] Boualem Benatallah, Quan Z. Sheng, Marlon Dumas. The Self-Serv Environment for Web Services Composition[J]. IEEE Internet Computing, 2003,7(1):40-48.
[5] Abhijit Patil, Swapna Oundhakar, Amit Sheth, et al. METEOR-S Web Service Annotation Framework[C]. The 13th International World Wide Web Conference, New York, USA: 533-562.
[6] Ponnekanti SR, Fox A. SWORD: A developer Toolkit for Web Service Composition[C]. In: Proc. of the Int'l World Wide Web Conf. Honolulu, 2002. 83-107
[7] B.Holtkamp, R.Gartmann, Y.Han. FLAME2008--Personalized Web Services for the Olympic Games 2008 in Beijing[C]. in Proc. eChallenges, e-2003, 2003.
[8] Erik Christensen, F.C., Greg Meredith, et al. Web Services Description Language (WSDL)1.1[R]. W3C. 2001.
[9] Martin Gudgin, M. H, SOAP Version 1.2 Part 1: Messaging Framework (Second Edition), [R]. W3C. 2007.
[10] Luc Clement, A. H., Claus von Riegen, et al. UDDI Version 3.0.2[R]. UDDI Spec Technical Committee Draft, [2004-10-19].
[11] S. Thatte. XLANG Web Services for Business Process Design[R]. OASIS. [2001-06-06].
[12] Frank Leymann. Web Services Flow Language (WSFL) 1.0[R]. IBM Software Group. 2001.
[13] A. Arkin. Business Process Modeling Language (BPML)1.0[R]. OASIS. 2003.
[14] A. Arkin, Scott Fordin,Wolfgang Jekeli. Web Service Choreography Interface (WSCI)1.0[R]. W3C. 2002.
[15] DAML Joint Committee. Daml Services (Daml-S)[R]. http://www.daml.org/services /owl-s/. 2003.
[16] D. Martin. OWL-S1.1[R]. http://www.daml.org/services/owl-s/l.1/. 2004.
[17] DAML Joint Committee. Daml+oil language[R]. http://www.daml.org/2001/03/ daml+oil-index.html. 2001.
[18] N. Kavantzas, D.Burdett. Web Services Choreography Description Language (WS-CDL) 1.0[R]. http://www.w3c.org/TR/ ws-cdl-10/. 2005.
[19] T.Andrews, F.Curbera, H.Dholakia, et al. Business Process Execution Language for Web Services (BPEL4WS) version 1.1[R]. http://xml.coverpages.org/bpel4ws.html. 2003.
[20] C.Yushi, L.E.Wah, D.K.Limbu. Web Services Composition- An Overview of Standards [J]. Synthesis Journal. 2005:137-150.
[21]吕庆中,韩燕波,麦中凡. Web服务环境中的业务过程建模语言比较框架.计算机工程与应用. 2003,23:7-13.
[22] Mendling, J., Müller, M., A Comparison of BPML and BPEL4WS, In: proceedings of the 1st Conference "Berliner XML-Tage", 2003, pages305-316.
[23] W.M.P., van der Aalst, etc. Web Service Composition Languages: Old Wine in New Bottles 29th EUROMICRO Conference: New Waves in System Architecture, 2003, pages 298-305.
[24] P. Wohed, W. M. P. v. d. A., M. Dumas, A.H.M ter Hofstede (2002). Pattern-Based Analysis of BPEL4WS.
[25] J. Rao and X. Su, A Survey of Automated Web Service Composition Methods, In: proceedings of the First International Workshop on Semantic Web Services and Web Process Composition, 2004.
[26] B. Srivastava and J. Koehler, Web Service Composition - Current Solutions and Open Problems, The 13th International Conference on Automated Planning & Scheduling (ICAPS), Italy, 2003.
[27] N. Milanovic and M. Malek, Current Solutions for Web Service Composition, Published by the IEEE Computer Society, 2004, www.informatik.hu-berlin.de/~milanovi/wscomp-survey-milanovic.pdf
[28] S. Majithia, M. Shields, etc., Triana: A Graphical Web Service Composition andExecution Toolkit, International Conference on Web Services, 2004.
[29] Cardoso, A. Sheth, Semantic e-Workflow Composition, Journal of Intelligent Information systems, 2003.
[30] D. Shuiguang, Managing Service flow in a Flexible, The 5th International Conference on Web Information Systems Engineering, 2004.
[31] S. Chadrasekaran, J. A. Miller, Composition, Performance Analysis and Simulation of Web Services, The International Journal of Electronic Commerce and Business Media, 2003.
[32] H. Yanbo, Z. Zhuofeng, etc., CAFISE: An Approach to Enabling Adaptive Configuration of Service Grid Applications, Journal of Computer Science and Technology, 2003.
[33] Sheila McIlraith, Tran Cao Son, Adapting Golog for Composition of Semantic Web Services, In: proceedings of the 8th International Conference on Knowledge Representation and Reasoning, 2002.
[34] W. M. P. Van Der Aalst, A. A. H. M. T. H., A. B. Kiepuszewski, Workflow Patterns, istributed Parallel Databases 14 (1), 2003.
[35] Evren Sirin, .etc, HTN Planning for Web Service Composition Using SHOP2, http://www.mindswap.org/papers/SHOP2JWS.
[36] J. Billington, S. Christensen, .etc, The Petri Net Markup Language: Concepts, Technology, and Tools. ICATPN 2003: 483-505.
[37] Arindam Banerji, .etc, (2002). Web Services Conversation Language (WSCL) 1.0. http://www.w3.org/TR/2002/NOTE-wscl10- 20020314/.
[38] Brahim Medjahed, Athman Bouguettaya, etc, Composing Web Services on the semantic web, The VLDB Journal, 2003, 12(4).
[39] Design/CPN, http://www.daimi.au.dk/designCPN/
[40] AT&T, Graphviz - Graph Visualization Software, 2005.
[41] Apache, X, The Document Object Model, 2005.
[42] X. Fu, T. Bultan and J. Su, Analysis of interacting BPEL Web Services, In: proceedings of the 13th International World Wide Web Conference, May 2004. ACM, pages 621-630.
[43] X. Fu, T. Bultan and J. Su, Synchronizability of conversations among Web Services, IEEE Transactions on Software Engineering, 31 December, 2005, (12):1042-1055.
[44] CPN tools. http://www.daimi.au.dk/CPNtools/
[45] D. Fahland and W. Reisig, ASM-based semantics for BPEL: The negative control flow, In proceedings of the 12th International Workshop on Abstract State Machines, 2005, pages 131-151.
[46]郭玉彬,杜玉越,奚建清,Web服务组合的有色网模型及运算性质,计算机学报,2006年第29卷07期.
[47] W. Reisig, Modeling and analysis techniques for Web Services and business processes, In: proceedings of the 7th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, 2005,vol.3535, pages 243-258.
[48] K. Jensen, Colored Petri Nets Basic Concepts, Analysis Methods and Practical Use, Volume 1, second edition, 1996.
[49] R. Kazhamiakin and M. PIstore, Parametric communication model for the verification of BPEL4WS compositions, In: Proceedings of the 2nd International Workshop on Web Services and Formal Methods, volume 3670 of Lecture Notes in Computer Science, 2005, pages 318-332.
[50] Hamadi R, Benatallah B, A Petri Net-Based Model for Web Service Composition, In: 4th Australasian Database Conf. (ADC2003), Adelaide, Australia, Conferences in Research and Practice in Information Technology, 2003, Vol.17.
[51] Zhang Jia, Chung Jen-Yao, Chang C. K., Kim S., WS-Net: A petri-net based specification model for Web Services, In: Proceedings of the 2nd IEEE International Conference on Web Servies, USA, 2004, 420-427.
[52] H. Foster, S. Uchitel, J. Magee and J. Kramer, Model-based Verification of Web Service Compositions, In: Proceedings of the 18th IEEE International Conference on Automated Software Engineering Conference (ASE 2003), 2003.
[53] Karamanolis C., Giannakopoulou D., Magee J., Wheater S. M, Model Checking of Workflow Schemas, Proc. of 4th IEEE/OMG International Enterprise Distributed Object Computing Conference (EDOC), 2000.
[54] H. Foster, S. Uchitel, J. Magee and J. Kramer, Compatibility for Web Service Choreography, presented at 3rd IEEE International Conference on Web Services (ICWS), San Diego, CA, 2004.
[55] Ferrara A, Web Services: A process algebra approach, In: Proceedings of the 2nd International Conference on Service Oriented Computing, 2004, pages 242-251.
[56]廖军,谭浩,刘锦德,基于PI-演算的Web服务组合的描述和验证,计算机学报,2005,28(4):635-642.
[57] Salaun G, Bordeaux L, Schaerf M, Describing and reasoning on Web Services using process algebra, In: Proceedings of the 2nd IEEE International Conference on Web Services, 2004, pages 43-51.
[58] A. Wombacher, P. Fankhauser and E. Neuhold, Transforming BPEL into annotated deterministic finite state automata for service discovery, In: Proceedings of the 2nd IEEE International Conference on Web Services, San Diego, CA, USA, July 2004, IEEE, pages 316-323.
[59]袁崇义,Petri网原理与应用.电子工业出版社,2005.
[60] Business Process Management Initiative,Business Process Modeling Language v1.0,2002,http://www.bpmi.org [61 Hamadi R,Benatallah B,A Petri Net-based Model for Web Services Composition,Proc. of the Fourteenth Australasian Database Conference on Database Technologies,2003
[62]郭小群,郝克刚,Web服务的PI-演算描述,计算机科学,Vol.33,No.3,2006
[63] Biplay S,Jana K,Web Services Compositon-Current Solution and Open Problems, http://www.zurich.ibm.com/pdf/ebizz/icaps-ws.pdf
[64] Web服务的业务流程执行语言版本1.1,2003年5月5日
[65] Tadao Murata,Petri Net: Properties、Analysis and Applications, Proceedings of the IEEE,1989,77(4):541-580
[66] Milner R,Communication and Concurrency,Englewood Cliffs:Prentice-Hall,1989
[67] Fensel D,The semantic Web and its languages,IEEE Intelligent Systems,2000,15(6):67-73
[68] Milner R,Communication and Mobile Systems:The PI-Calculus, Cambridge University Press,1999
[69] Milner R,Parrow J,Walker D,A calculus of mobile processes, part I/II,Journal of Information and Computation,1992,100(1):1-77
[70] Lin Hui-Min,Complete proof systems for observation congruences in finite control PI-calculus,Proceedings of the 25th International Colloquium on Automata,Languages and Programming,Aalborg,Denmark,1998,442-450
[71] Jiao Wen-PIn,Zhou Ming-Hui,Wang Qian-Xiang,Formal framework for adaptivemulti-agent Systems,Proceedings of IEEE/WIC International Conference on Intelligent Agent Technology,Halifax,Canada,2003
[72] Makus Lumpe,A PI-calculus based approach to software composition,Institute of Computer Science and Applied Mathematics,University of Bern,Switzerland,1999
[73] Bjorn Victor,The Mobility Workbench User’s Guide Polyadic version 3.122,1994
[74] Bjorn Victor,Faron Moller. The Mobility Workbench-A Tool for the PI-Calculus,1994
[75] Bjorn Victor,A Verification Tool for the Polyadic PI-Calculus. May 9,1994
[76]李东来,王丰锦,韩燕波,基于Web服务的动态工作流系统中资源管理问题,计算机工程,Vol.29,No.18,2003年10月
[77]石静,丁长明,赵泽宇,薛向阳,Web服务合成研究综述,计算机科学,vol.31,No.6,2004
[78] Benatallah B,Dumas M,Declarative Compositon and Peer-to-Peer Provisioning of Dynamic Web Services, Proc.of the 18th Intl.conf,Data Engineering(ICDE.02),IEEE Computer Society,2002
[79] Chakraborty D,Joshi A,Dynamic Service Compositon: State-of-the-Art and Research Directions:[Technical Report TR-CS-01-19]UMBC,December,2001, http://research.ebiquity.org/re/papers.html
[80] Benjamin C.PIerce,Programming in the PI-Calculus,Department of Computer Science University of Edinburgh
[81] Robin Milner,The Polyadic PI-Calculus:a Tutorial,Laboratory for Foundations of Computer Science,Computer Science Department,University of Edinburgh,The King’s Buildings Edinburgh EH9 3JZ,UK,October,1991
[82] Fredrick B.Beste,The Model Prover-a sequent-calculus based modal PI-calculus model checker tool for finite control PI-calculus agents,1998.1.9
[83] Gian Luca Cattani,Ian Stark and Glynn Winskel,Presheaf Models for the PI-Calculus,BRICS,Department of Computer Science,University of Aarhus,Denmark,December,1997
[84] Lucian WIschik,New directions in implementing the PI-calculus,University of Bologna,30th,August,2002
[85] T.Andrews,F.Curbera,H.Dholakia,Y.Goland,J.Klein,F.Leymann,K.Liu,D.Roller,D.Smith,S.Thatte,I.Trickovic,and S.Weerawarana,Business Process execution language for WebServices,version1.1, http://www-128.ibm.com/developerworks/webservices/library/ws-bpel/index.html, 2003.5
[86] Nickolas Kavantzas.etal,Web Services Choreography Description Language Version 1.0,2004
[87] Orava F,Parrow J,An algebraic verification of a mobile network,Formal Aspect of Computing,1992,4(6)
[88]廖军,谭浩,刘锦德,基于PI-演算的Web服务可替换性验证,华中科技大学学报(自然科学版)Vol.33, 2005.12
[89] Riccardo Pucella,Notes on Programming Standard ML of New Jersey(version 110.0.6), 2001, http://www.cs.cornell.edu/riccardo/prog-smlnj/notes-011001.pdf
[90] Raymond Devillers,Hanna Klaudel,Maciej Koutny,Petri net semantics of the finite PI-calculus,School of Computing Science,University of Newcastle upon Tyne,June 2004