Web服务组合形式化模型研究
|
摘要
随着Web服务技术的迅速发展,越来越多的的Web服务运行在Internet上,但单个的Web服务功能有限,难以满足日益增长和不断变化的用户需求。因此,如何将已有的、运行在异构平台上的Web服务组合起来,以提供给用户更为强大和增值的功能,成为Web服务研究领域中的一个热点。
由于已有的Web服务可能是彼此独立地开发,以不同语言实现,运行在不同的、异构的平台上,因此Web服务组合存在的问题有:如何描述Web服务的动态行为,如何定义和描述Web服务间的交互的逻辑顺序以保证Web服务的动态行为的匹配性,如何保证Web服务之间传递消息的数据类型的一致性,如何对组合的Web服务进行验证和测试以确保执行结果的正确性。
目前已经提出的Web服务组合规范如BPEL4WS、WS-CDL都是基于XML的描述性语言,缺乏一种形式化模型来表达语言的语义以及形式化验证方法来保证用这些规范所定义的Web服务组合的正确性。同时,由于参与Web服务组合的各个子服务都运行在分布式异构的环境下,因此想依靠组合的Web服务的实际运行来检测组合中的错误是代价昂贵的并且几乎是不可能的,因此对Web服务组合的形式化验证也是必须的而且是非常重要的。
解决上述问题的一个行之有效的办法就是针对Web服务组合规范如BPEL4WS、WS-CDL建立合适的形式化模型,形式化地定义和描述Web服务组合的动态交互行为,利用Web服务组合的形式化模型对Web服务组合的性质如死锁避免、数据类型一致性和动态行为的匹配性进行检查和验证,以保证Web服务组合的动态行为的匹配和数据类型的一致性。
因此,针对Web服务组合规范BPEL4WS和WS-CDL,研究了基于工作流的Web服务组合形式化模型以及如何利用Web服务组合的形式化模型对Web服务组合的动态行为的匹配和数据类型的一致性进行验证。
针对Web服务组合规范BPEL4WS,分别建立了BPEL4WS到Pi-演算和CSP的概念映射,在此基础上,建立了基于Pi-演算和CSP的BPEL4WS形式化模型;同时给出了从BPEL4WS到Pi-演算和CSP进程的自动转换算法和模型的验证方法。
针对Web服务组合规范WS-CDL,建立了基于全局的形式化模型框架AbstractWS-CDL,在此基础上利用Abstract WS-CDL对WS-CDL中各类行为进行了形式化描述;同时定义了将全局模型框架Abstract WS-CDL映射到基于Pi-演算的局部BPEL4WS模型的映射规则,并给出了全局模型框架和局部模型一致性的形式化定义;然后给出了全局和局部二个层次的模型验证方法以及全局模型框架和局部模型一致性的验证方法。
利用基于Pi-演算的形式化方法研究和给出了二个Web服务的强互相容和弱互相容的形式化定义,在二个Web服务弱互相容定义的基础上,定义了二个Web服务之间互投影的算法,进而给出了多个Web服务互相容的形式化定义;然后给出了Web服务的可替换性的判断准则和二个Web服务相容性的检测算法。
研究和给出了类型化的BPEL4WS形式化模型和类型化的Abstract WS-CDL形式化模型框架,特别是提出了进程类型假设集的外延和进程类型假设集相容性的概念,并且给出了进程类型假设集的合并算法;在此基础上,定义了全局会话和局部进程类型良好性的推理规则和捕获由于类型不一致而导致运行时错误的操作语义。同时,给出了从类型化的全局模型框架到类型化的局部模型的映射规则;然后,针对类型化的Abstract WS-CDL,给出了全局会话类型安全性质的证明。
根据所建立的全局和局部模型,给出了一个自顶向下的Web服务组合实现框架iFrame4WS,在该框架中将Web服务组合的过程划分为描述层、抽象层和执行层,并通过抽象层的形式化模型和形式化验证来保证Web服务组合的的动态行为的匹配和数据类型的一致性。
With the rapid development of web services technology, increasing amounts of web services are running over Internet. But the limited function of single web service can not satisfy the growing and varying custom requirement. Therefore, how to compose existed web services running on heterogeneous platforms together so as to provide custom more powerful and valuable function has become hotspot of web service researching area.
Because web services may be developed independently, implemented with different languages and running on heterogeneous platforms, there exist following problems about web services composition: how to describe the dynamic behavior of web service, how to define and describe the logical sequence of interaction between web services in order to guarantee the compatibility of web service’s dynamic behavior, how to verify and check web services composition in order to guarantee the correctness of composite web service’s execution.
The proposed web service composition specifications such as BPEL4WS and WS-CDL so far are XML-based descriptive languages, lacking some kind of formal model to express the semantic of these languages accurately and formal verification mechanism to ensure the correctness of composite web service defined by such web service composition specifications. Moreover,it is cost expensive and nearly impossible to find out web service composition errors only depend upon composite web service’s actual running because the participates in the web services composition are all running in heterogeneous distributed environment. Therefore, it is important and necessary to formally verify the web services composition.
An effective means to deal with the problems mentioned above is to present formal model according to web service composition specifications such as BPEL4WS, WS-CDL, et al respectively, formally define and describe the dynamic interaction behavior of web services composition, verify the properties of web service composition like deadlock avoidance, consistency of data type and dynamic behavior’s compatibility utilizing formal model of web service composition so that the compatibility of dynamic interaction behavior of web services composition and consistency of data type can be guaranteed.
Accordingly, the workflow based formal model of web services composition specification BPEL4WS and WS-CDL and the verification of the web services composition based on the formal model is studied.
Aiming at web service composition specification BPEL4WS, we define the conception mapping from BPEL4WS to Pi-calculus and CSP respectively. Furthermore, not only the formal models of BPEL4WS based on Pi-calculus and CSP but also the automatic translation algorithm from BPEL4WS to Pi-calculus and CSP are presented. The model verification method is also presented through case study.
Aiming at web service composition specification WS-CDL, we propose a formal model framework Abstract WS-CDL that is based on global view and formally describe all activities defined in WS-CDL specification. A set of rules for mapping global based formal model framework Abstract WS-CDL to local model depicted by Pi-Calculus and formal definition of conformance between global model and local model are also defined. The model verification methods at global level and local level are presented through a case study.
We analyzes web services compatibility using a formal approach based on Pi-calculus and present formal definitions of strong compatibility and weak compatibility between two web services. On the basis of weak compatibility between two web services, the projection operation algorithm between two web services is defined and the formal definitions of compatibility between multiple web services on the base of projection operation is proposed furthermore. According to the formal definitions of compatibility between multiple web services, the web service substitutability is characterized formally. The checking algorithm of compatibility between two web services is also taken into account.
On the basis of presented formal model of BPEL4WS and WS-CDL, we study and present typed formal models of BPEL4WS and WS-CDL. Particularly, we propose the concepts of type assumption set extension and type assumption set compatibility, and define the merging algorithm of type assumption set accordingly. On the ground of merging algorithm of type assumption set, we define the reduction rules for well type judgments of global session and local process, and the operational semantics for capturing run-time error due to date type mismatch. A set of typed rules for mapping typed global model framework to typed local model are defined. The type safety property of Abstract WS-CDL session is also proved.
On the basis of presented formal model of BPEL4WS and WS-CDL, we outline a Top-Down framework- iFrame4WS for web services composition implementation. In iFrame4WS, the process of web services composition is divided into description level, abstract level and execution level. The formal model and verification approach are defined in abstract level so as to ensure the compatibility of dynamic interaction behavior of web services composition and consistency of data type.
由于已有的Web服务可能是彼此独立地开发,以不同语言实现,运行在不同的、异构的平台上,因此Web服务组合存在的问题有:如何描述Web服务的动态行为,如何定义和描述Web服务间的交互的逻辑顺序以保证Web服务的动态行为的匹配性,如何保证Web服务之间传递消息的数据类型的一致性,如何对组合的Web服务进行验证和测试以确保执行结果的正确性。
目前已经提出的Web服务组合规范如BPEL4WS、WS-CDL都是基于XML的描述性语言,缺乏一种形式化模型来表达语言的语义以及形式化验证方法来保证用这些规范所定义的Web服务组合的正确性。同时,由于参与Web服务组合的各个子服务都运行在分布式异构的环境下,因此想依靠组合的Web服务的实际运行来检测组合中的错误是代价昂贵的并且几乎是不可能的,因此对Web服务组合的形式化验证也是必须的而且是非常重要的。
解决上述问题的一个行之有效的办法就是针对Web服务组合规范如BPEL4WS、WS-CDL建立合适的形式化模型,形式化地定义和描述Web服务组合的动态交互行为,利用Web服务组合的形式化模型对Web服务组合的性质如死锁避免、数据类型一致性和动态行为的匹配性进行检查和验证,以保证Web服务组合的动态行为的匹配和数据类型的一致性。
因此,针对Web服务组合规范BPEL4WS和WS-CDL,研究了基于工作流的Web服务组合形式化模型以及如何利用Web服务组合的形式化模型对Web服务组合的动态行为的匹配和数据类型的一致性进行验证。
针对Web服务组合规范BPEL4WS,分别建立了BPEL4WS到Pi-演算和CSP的概念映射,在此基础上,建立了基于Pi-演算和CSP的BPEL4WS形式化模型;同时给出了从BPEL4WS到Pi-演算和CSP进程的自动转换算法和模型的验证方法。
针对Web服务组合规范WS-CDL,建立了基于全局的形式化模型框架AbstractWS-CDL,在此基础上利用Abstract WS-CDL对WS-CDL中各类行为进行了形式化描述;同时定义了将全局模型框架Abstract WS-CDL映射到基于Pi-演算的局部BPEL4WS模型的映射规则,并给出了全局模型框架和局部模型一致性的形式化定义;然后给出了全局和局部二个层次的模型验证方法以及全局模型框架和局部模型一致性的验证方法。
利用基于Pi-演算的形式化方法研究和给出了二个Web服务的强互相容和弱互相容的形式化定义,在二个Web服务弱互相容定义的基础上,定义了二个Web服务之间互投影的算法,进而给出了多个Web服务互相容的形式化定义;然后给出了Web服务的可替换性的判断准则和二个Web服务相容性的检测算法。
研究和给出了类型化的BPEL4WS形式化模型和类型化的Abstract WS-CDL形式化模型框架,特别是提出了进程类型假设集的外延和进程类型假设集相容性的概念,并且给出了进程类型假设集的合并算法;在此基础上,定义了全局会话和局部进程类型良好性的推理规则和捕获由于类型不一致而导致运行时错误的操作语义。同时,给出了从类型化的全局模型框架到类型化的局部模型的映射规则;然后,针对类型化的Abstract WS-CDL,给出了全局会话类型安全性质的证明。
根据所建立的全局和局部模型,给出了一个自顶向下的Web服务组合实现框架iFrame4WS,在该框架中将Web服务组合的过程划分为描述层、抽象层和执行层,并通过抽象层的形式化模型和形式化验证来保证Web服务组合的的动态行为的匹配和数据类型的一致性。
With the rapid development of web services technology, increasing amounts of web services are running over Internet. But the limited function of single web service can not satisfy the growing and varying custom requirement. Therefore, how to compose existed web services running on heterogeneous platforms together so as to provide custom more powerful and valuable function has become hotspot of web service researching area.
Because web services may be developed independently, implemented with different languages and running on heterogeneous platforms, there exist following problems about web services composition: how to describe the dynamic behavior of web service, how to define and describe the logical sequence of interaction between web services in order to guarantee the compatibility of web service’s dynamic behavior, how to verify and check web services composition in order to guarantee the correctness of composite web service’s execution.
The proposed web service composition specifications such as BPEL4WS and WS-CDL so far are XML-based descriptive languages, lacking some kind of formal model to express the semantic of these languages accurately and formal verification mechanism to ensure the correctness of composite web service defined by such web service composition specifications. Moreover,it is cost expensive and nearly impossible to find out web service composition errors only depend upon composite web service’s actual running because the participates in the web services composition are all running in heterogeneous distributed environment. Therefore, it is important and necessary to formally verify the web services composition.
An effective means to deal with the problems mentioned above is to present formal model according to web service composition specifications such as BPEL4WS, WS-CDL, et al respectively, formally define and describe the dynamic interaction behavior of web services composition, verify the properties of web service composition like deadlock avoidance, consistency of data type and dynamic behavior’s compatibility utilizing formal model of web service composition so that the compatibility of dynamic interaction behavior of web services composition and consistency of data type can be guaranteed.
Accordingly, the workflow based formal model of web services composition specification BPEL4WS and WS-CDL and the verification of the web services composition based on the formal model is studied.
Aiming at web service composition specification BPEL4WS, we define the conception mapping from BPEL4WS to Pi-calculus and CSP respectively. Furthermore, not only the formal models of BPEL4WS based on Pi-calculus and CSP but also the automatic translation algorithm from BPEL4WS to Pi-calculus and CSP are presented. The model verification method is also presented through case study.
Aiming at web service composition specification WS-CDL, we propose a formal model framework Abstract WS-CDL that is based on global view and formally describe all activities defined in WS-CDL specification. A set of rules for mapping global based formal model framework Abstract WS-CDL to local model depicted by Pi-Calculus and formal definition of conformance between global model and local model are also defined. The model verification methods at global level and local level are presented through a case study.
We analyzes web services compatibility using a formal approach based on Pi-calculus and present formal definitions of strong compatibility and weak compatibility between two web services. On the basis of weak compatibility between two web services, the projection operation algorithm between two web services is defined and the formal definitions of compatibility between multiple web services on the base of projection operation is proposed furthermore. According to the formal definitions of compatibility between multiple web services, the web service substitutability is characterized formally. The checking algorithm of compatibility between two web services is also taken into account.
On the basis of presented formal model of BPEL4WS and WS-CDL, we study and present typed formal models of BPEL4WS and WS-CDL. Particularly, we propose the concepts of type assumption set extension and type assumption set compatibility, and define the merging algorithm of type assumption set accordingly. On the ground of merging algorithm of type assumption set, we define the reduction rules for well type judgments of global session and local process, and the operational semantics for capturing run-time error due to date type mismatch. A set of typed rules for mapping typed global model framework to typed local model are defined. The type safety property of Abstract WS-CDL session is also proved.
On the basis of presented formal model of BPEL4WS and WS-CDL, we outline a Top-Down framework- iFrame4WS for web services composition implementation. In iFrame4WS, the process of web services composition is divided into description level, abstract level and execution level. The formal model and verification approach are defined in abstract level so as to ensure the compatibility of dynamic interaction behavior of web services composition and consistency of data type.
引文
[1] M.N. Huhns, M.P. Singh. Service-Oriented Computing: Key Concepts and Principles. IEEE Internet Computing, 2005, 9:75-81
[2] M.P Papazoglou. Service-oriented computing: Introduction. Communications of the ACM, 2003, 46(10):24-28
[3] M.P Papazoglou. Service-oriented computing: Concepts, characteristics and directions. In Proceedings of the 4th International Conference on Web Information System Engineering, Roma, Italy, 2003. Washington DC,USA:IEEE Computer Society Press, 2003: 3-10
[4] C. Ferris, J. Farrell. What are Web services? Communications of the ACM, 2003,46(6):31
[5] E. Christensen, F. Curbera, G. Meredith, S. Weerawarana. Web Services Description Language (WSDL) 1.1. http://www.w3.org/TR/2001/NOTE-wsdl-20010315
[6] N. Mitra, Y. Lafon. SOAP Version 1.2 Part 0: Primer (Second Edition). http://www.w3.org/TR/soap12-part0/
[7] L. Clement, A. Hately, C.V. Riegen, T. Rogers. UDDI Version 3.0.2., UDDI Spec Technical Committee Draft.http://uddi.org/pubs/uddi-v3.0.2-20041019.htm
[8] B. Srivastava, J.Koehler. Web Service Composition-Current Solutions and Open Problems. In Proceedings of the 13th International Conference on Automated Planning & Scheduling, Trento, Italy, 2003. California, USA:Advancement of Artificial Intelligence Press, 2003:28-35
[9] D. Beckett, Brian McBride. RDF/XML Syntax Specification (Revised). http://www.w3.org/TR/rdf-syntax-grammar/
[10] D. Martin, M. Burstein, J. Hobbs, O. Lassila, et al. OWL-S: Semantic Markup for Web Services. http://www.w3.org/Submission/OWL-S/
[11] S. McIlraith, T. Son. Adapting Golog for composition of semantic Web services. In: D. Fensel, F. Giunchiglia, D.L. McGuinness, et al, eds. Proceedings of the 8thInternational Conference on Principles of Knowledge Represantation and Reasoning, Toulouse, France, 2002. California, USA:Morgan Kaufmann, 2002:482-493
[12] F. Leymann. Web Services Flow Language (WSFL 1.0). http://xml.coverpages.org/WSFL-Guide-200110.pdf
[13] A. Arkin, S. Askary, S. Fordin, et al. Web Service Choreography Interface (WSCI) 1.0. http://www.w3.org/TR/wsci/
[14] T. Andrews, F. Cubera, H. Dholakia, et al. Business Process Execution Language for Web Services Version1.1.http://www-128.ibm.com/developerworks/library/specification/ws-bpel/
[15] N. Kavantzas, D. Burdett, G. Rizinger, et al. Web Service Choreography Description Language Version 1.0. http://www.w3.org/TR/ws-cdl-10/
[16] A. Arkin. Business Process Modeling Language. http://xml.coverpages.org/BPML-2002.pdf
[17] A. Bucchiarone, S. Gnesi. A Survey on Services Composition Languages and Models. In Proceedings of the International Workshop on Web Services Modeling and Testing, Palermo, Italy, 2006:51-63
[18] R. Dijkman, M. Dumas. Service-oriented Design: A Multi-viewpoint Approach. International Journal of Cooperative Information Systems, 2004, 13(4): 337-368
[19] R. Hull, J.Su.Tools for Composite Web Services: A Short Overview. ACM SIGMOD Record, 2005, 34(2):86-95
[20]岳昆,王晓玲,周傲英. Web服务核心支撑技术:研究综述.软件学报, 2004, 15(3):428-442
[21]饶云,冯博琴,李尊朝.基于Web Services的服务合成技术综述.系统工程与电子技术, 2005, 27(8):1481-1489
[22] W.M.P. van der Aalst, M. Dumas, A.H.M. ter Hofstede. Web Service Composition Languages: Old Wine in New Bottles? Lecture Notes in Computer Science, 2003, 2593:59-72
[23] J.C.M Baeten. A brief history of process algebra. Theoretical Computer Science, 2005, 335(2-3):131-146
[24] R.Hamadi, B.Benatallah. A Petri Net-based Model for Web Service Composition. In: K. Schewe, Xiaofang Zhou, eds. Proceedings of 14th Australasian DatabaseConference on Database Technologies, Adelaide, Australia, 2003. Australian Computer Society: 2003(17):191-200
[25] W.M.P van der Aalst, A.H.M. ter Hofstede. Verification of Workflow Task Structures: A Petri-Net-Based Approach. Information Systems, 2000, 25(1):43-69.
[26] W.M.P van der Aalst. Woflan: A Petri-net-based Workflow Analyzer. Systems Analysis, Modeling, Simulation, 1999, 35(3):345-357.
[27] H.M.W. Verbeek, T. Basten, W.M.P. van der Aalst. Diagnosing workow processes using Woan. The Computer Journal, 2001, 44(4):246-279
[28] D.Berardi, D.Calvanese, G. De Giacomo,et al. Automatic Composition of e-Services that Export their Behavior. Lecture Notes in Computer Science, 2003, 2910:43-58
[29] D.Berardi, D.Calvanese, G. De Giacomo,et al. Automatic Services Composition based on Behavior Descriptions. International Journal of Cooperative Information Systems, 2005, 14(4):333-376
[30] D.Berardi, G. De Giacomo, M. Lenzerini, et al. Synthesis of underspecified composite e-services based on automated reasoning. In:M. Aiello, M. Aoyama, F. Curbera, et al, eds. Proceedings of 2th International Conference on Service-Oriented Computing, New York, USA, 2004. ACM Press, 2004:105-114
[31] G. De Giacomo, M. Lenzerini. PDL-based framework for reasoning about actions. Lecture Notes in Artificial Intelligence, 1995, 992:103-114
[32] J.E. Hopcroft, R. Motwani, J.D. Ullman. Introduction to Automata Theory, Languages, and Computation (2nd Edition). Boston,USA:Addison Wesley, 2000
[33] T.Bultan, X.Fu, R.Hull, J.Su. Conversation Specfication: A new approach to design and analysis of e-service composition. In Proceedings of 12th International Conference on World Wide Web, Budapest, Hungary, 2003. ACM Press, 2003:403-410
[34] X.Fu, T.Bultan, J.Su. Conversation protocols: A formalism for specification and verification of reactive electronic services. In: O.H. Ibarra, Zhe Dang, eds. Proceedings of 8th International Conference on Implementation and Application of Automata, California, USA, 2003. Spinger, Lecture Notes in Computer Science, 2003,2759:188-200
[35] G. Plotkin. Call-by-name, call-by-value, and theλ-Calculus. Theoretical Computer Science, 1975, 1:125-159
[36] C.A.R Hoare. Communicating Sequential Processed. Commucation of the ACM. 1978,21(8):666-677
[37] C.A.R. Hoare. Communicating Sequential Processes. New Jersey,USA: Prentice-Hall, 1985
[38] R. Milner. A Calculus of Communicating Systems. Lecture Notes in Computer Science, 1980, Volume 92
[39] R. Milner, J.Parrow, D. Walker. A calculus of mobile process (PartsⅠandⅡ). Information and Computation, 1992, 100:1-77
[40] R. Milner. Communicating and Mobile Systems: The Pi Calculus. Cambridge: Cambridge University Press, 1999.
[41] T. Bolognesi, E. Brinksma. Introduction to the ISO Specification Language LOTOS. Computer Network and ISDN Systems, 1987, 14:25-59
[42] G. Salaün, L. Bordeaux, M. Schaerf. Describing and Reasoning on Web Services using Process Algebra. In Proceedings of the 2th IEEE International Conference on Web Services, California, USA, 2004. Washington DC,USA:IEEE Computer Society Press, 2004:43-50
[43] S. Schneider, J. Davis, D.M. Jackson, et al. Timed CSP: Theory and Practice. Lecture Notes in Computer Science, 1992, 600:640-675
[44] A. Ferrara. Web services: a process algebra approach. In: M. Aiello, M. Aoyama, F. Curbera, et al, eds. Proceedings of 2th International Conference on Service Oriented Computing, New York, USA, 2004. ACM Press, 2004: 242-251
[45] G. Salaün, A. Ferrara, and A. Chirichiello. Negotiation among web services using LOTOS/CADP. Lecture Notes in Computer Science, 2004, 3250:198-212
[46] L. Bordeaux and G. Salaün. Using process algebra for web services: Early resultsand perspectives. Lecture Notes in Computer Science, 2004, 3324:54-68
[47] A. Brogi, C. Cannl, E. Pimentel. Formalizing Web Service Choreographies. ElectronicNotes in Theoretical Computer Science, 2004, 105: 73-94
[48] H. Foster, S. Uchitel, J. Magee, et al. Model based verification of web service compositions. In Proceedings of 18th International Conference on Automated Software Engineering, Montreal, Canada, 2003.Washington DC,USA:IEEE Computer Society Press, 2003: 152-163
[49] H. Foster, S. Uchitel, J. Kramer, et al. Compatibility verification for web service choreography. In Proceedings of the 2th International Conference on Web Services, California, USA, 2004. Washington DC, USA:IEEE Computer Society Press, 2004:738-741
[50] H. Foster, S. Uchitel, J. Magee, et al. Using a rigorous approach for engineering web service compositions: a case study. In Proceedings of the 2005 IEEE International Conference on Services Computing, Orlando, USA, 2005. Washington DC, USA: IEEE Computer Society Press, 2005, 1: 217-224.
[51] H. Foster, S. Uchitel, J. Magee,et al. Model-Based analysis of Obligations in Web Service Choreography. In Proceedings of the Advanced International Conference on Telecommunications and International Conference on Internet and Web Applications and Services, Guadeloupe, French, 2006. Washington DC, USA: IEEE Computer Society Press, 2006:149-157
[52] M. Koshkina, F. van Breugel. Modelling and verifying web service orchestration by means of the concurrency workbench. ACM SIGSOFT Software Engineering Notes, 2004, 29(5):1-10
[53] M. Koshkina. Verification of business processes for web services [Master's thesis]. Toronto, Canada:York University, 2003
[54] M. Viroli. Towards a formal foundation to orchestration languages. In Proceedings of the first International Workshop on Web Services and Formal Method, Pisa, Italy, 2004. Elsevier, Electronic Notes in Theoretical Computer Science, 2004, 15:51-71
[55] E. Oren, A. Haller. Formal Frameworks for Workflow Modelling [DERI Technical Report 2005-4-07]. Galway, Ireland: Digital Enterprise Research Institude, National University of Ireland, 2005
[56] F. Puhlmann. Why do we actually need the Pi-Calculus for Business Process Management? In:W. Abramowicz, H.C. Mayr, eds. Proceedings of 9th International Conference on Business Information Systems (BIS 2006), Klagenfurt, Austria, 2006. Lecture Notes in Informatics, 2006, 85: 77-89
[57] F. Puhlmann, M. Weske. Using the Pi-Calculus for Formalizing Workflow Patterns. In Proceedings of 3th International Conference on Business Process Management , Nancy, France, 2005: 153-168
[58] H. Overdick, F. Puhlmann,M. Weske. Towards a Formal Model for Agile Service Discovery and Integration. In Proceedings of first International ICSOC Workshop on Dynamic Web Processes (ICSOC-DWP05), Amsterdam, Netherlands, 2005
[59] S.J. Woodman, D.J. Palmer, S.K. Shrivastava, et al. Notations for the Specification and Verification of Composite Web Services. In Proceedings of the 8th IEEE International Enterprise Distributed Object Computing Conference., California, USA, 2004. Washington DC,USA:IEEE Computer Society Press, 2004:35-46
[60] J. Camara, C. Canal, J.Cubo. Issues in the formalization of Web Service Orchestrations. In Proceedings of 2th International Workshop on Coordination and Application Techniques for Software Entities, Glasgow, Scotland, 2005:17-24
[61] Y. Yang, Q. Tan, and Y. Xiao. Verifying web services composition. Lecture Notes in Computer Science, 2005, 3770: 354-363
[62] Y. Yang, Q. Tan, and Y. Xiao. Verifying web services composition based on hierarchical colored Petri nets. In:A. Hahn, S. Abels, L. Haak, eds. Proceedings of the first International ACM Workshop on Interoperability of Heterogeneous Information Systems, Bremen, Germany, 2005. ACM Press, 2005: 47-54
[63] Yang, Q. Tan, Y. Xiao, J. Yu, and F. Liu. Exploiting hierarchical CP-nets to increase reliability of web services workflow. In Proceeding of the International Symposium on Applications and the Internet, Phoeniz, AZ, USA, 2006. Washington DC, USA:IEEE Computer Society Press, 2006:116-122
[64]张文涛,彭泳,陈俊亮.基于Petri网的Web服务自动组合研究.计算机学报, 2006, 29(7):1058-1066
[65]张文涛,彭泳,陈俊亮.会话类E-Service的接口兼容和服务组合分析.计算机学报, 2006, 29(7):1047-1056
[66]杨鑫,陈俊亮. WSC/ADL:Web服务组合系统体系结构描述语言.软件学报, 2006, 17(5):1182-1194
[67]陈彦萍,李增智,唐亚哲等.一种满足马尔可夫性质的不完全信息下的Web服务组合方法.计算机学报, 2006, 29(7):1167-1178
[68]陈彦萍,李增智,郭志胜. Web服务组合中基于服务质量的服务选择算法.西安交通大学学报, 2006, 40(8):897-905
[69]漆玉松,钱柱中,是湘全.基于Agent的Web服务组合研究.南京理工大学学报, 2006, 30(3):315-319
[70]廖军,谭浩,刘锦德.基于Pi-演算的Web服务组合的描述和验证.计算机学报, 2005, 28(4):635-643
[71] J.C.M Baeten, W.P. Weijand. Process Algebra. Cambridge Tracts in Theoretiacl Computer Science, volume 18. Cambridge, England:Cambridge University Press, 1990
[72] G. Winskel. The Formal Semantics of Programming Languages: An Introduction. Massachusetts, USA: The MIT Press, 1993
[73] G. Plotkin. A structural approach to operational semantics [Technical Report DAIMI FN-19], Aarhus, Denmark: Computer Science Department, Aarhus University, 1981.
[74] D.Turi, G.Plotkin. Towards a Mathematical Operational Semantics. In Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, 1997. Washington DC, USA:IEEE Computer Society Press, 1997:280-291
[75] R.D Tennent. The denotaional semantics of programming languages. Communication of the ACM, 1976, 19(8):437-453
[76] S. Owicki, D. Gries, Verifying properties of parallel programs: an axiomatic approach, Communications of the ACM, 1976, 19(5):279-285
[77] P. Wohed, W.M.P van de Aalst, M. Dumas, et al. Pattern Based Analysis of BPEL4WS [FIT-TR-2002-04 Technical Report]. Queensland, Australia:Queensland University of Technology, 2003
[78] D. SANGIORGI. A Theory of Bisimulation for the pi-Calculus. Acta Informatica, 1996, 3(1): 69-97
[79] M.Hennessy, H. Lin. Symbolic bisimulations, Theoretical Computer Science, 1995, 138(2): 353-369
[80] Yuxi Fu. Bisimulation congruence of Pi-calculus, Information and Computation, 2003, 184(1):201-226
[81] B. Victor. A Verification Tool for the Polyadic Pi-Calculus [DoCS Licentiate thesis 94/50]. Uppsala, Sweden: Department of Computer Systems, Uppsala University, 1994
[82] B. Victor, F. Moller. The Mobility Workbench-A Tool for the Pi-Calculus. In: D.Dill, ed. Proceedings of the 6th International Conference on Computer Aided Verification, California, USA, 1994. Springer, Lecture Notes in Computer Science, 1994, 818:428-440
[83] M. Dam. Model Checking Mobile Processes. Lecture Notes in Computer Science, 1993, 715:22-36
[84] A. Barros, M. Dumas, P. Oaks. A Critical Overview of the Web Services Choreography Description Language (WS-CDL). Business Process Trends, 2005. http://www.bptrends.com
[85] J. Mendling, M. Hafner. From WS-CDL Choreography to BPEL Process Orchestration. http://wi.wu-wien.ac.at/home/mendling/publications/TR06-CDL.pdf
[86] N. Busi, R. Gorrieri, C. Guidi, et al. Towards a formal framework for Choreography. In Proceedings of the 14th IEEE International Workshops on Enabling Technologies: Infrastructures for Collaborative Enterprises (WETICE-2005), Linkoping, Sweden, 2005. Washington DC,USA:IEEE Computer Society Press, 2005: 107-112
[87] R. Gorrieri, C. Guidi, R. Lucci. Reasoning about interaction patterns in Choreography. In: M. Bravetti, L. Kloul, G. Zavattaro, eds. Proceedings of 2th International Workshop on Web Services and Formal Methods (WS-FM '05), Versailles, France, 2005. Springer, Lecture Notes in Computer Science, 2005, 3670:333-348
[88] W.L Yeung, J. Wang, W. Dong. Verifying Choreographic Descriptions of WebServices Based on CSP. In Proceedings of the IEEE Services Computing Workshops (SCW'06), 2006. Washington DC,USA:IEEE Computer Society Press, 2006:97-104
[89] M. Baldoni, C. Baroglio, A. Martelli, et al. Verifying the Conformance of Web Services to Global Interaction Protocols: A First Step. In Proceedings of the 2th International WorkShop on Web Services and Formal Methods, Versailles, France, 2005. Springer, Lecture Notes in Computer Science, 2005, 3670:257-271
[90] Xiangpeng Zhao, Hongli Yang, Zongyan Qiu. Towards the Formal Model and Verification of Web Service Choreography Description Language. In: M. Bravetti, M. Nú?ez, G. Zavattaro, eds. Proceedings of the 3th International Workshop on Web Service and Formal Methods, Vienna, Austria, 2006. Springer, Lecture Notes in Computer Science, 2006, 4184:273-287
[91] L.Bordeaux, G.Salaün, D.Berardi, et al. When are two Web Services Compatible? In: Ming-Chien Shan, U.Dayal, M. Hsu, eds. Proceedings of the 5th International Workshop on Technologies for E-Services, Toronto, Canada, 2004. Springer, Lecture Notes in Computer Science, 2004, 3324:15-28
[92] Yuliang Shi, Liang Zhang, Fangfang Liu, et al. Compatibility Analysis of Web Services. In: A. Skowron, R. Agrawal, M. Luck, et al, eds. Proceedings of the 2005 IEEE/WIC/ACM International Conference on Web Intelligence, Compiěgne, France, 2005. Washington DC,USA:IEEE Computer Society Press, 2005:483-486
[93] Fangfang Liu, Liang Zhang, Yuliang Shi, et al. Formal analysis of Compotibility of Web Services via CCS. In Proceedings of the International Conference on Next Generation Web Services Practices, Seoul, Korea, 2005. Washington DC, USA: IEEE Computer Society Press, 2005:143-148
[94] YunYao Li, H.V. Jagadish. Compatibility Determiation in Web Services. In Proceedings of the first International E-Services Workshop, Pittsburgh, USA, 2003:7-15
[95] C.Canal, L.Fuentes, E.Pimentel, et al. Adding Roles to CORBA Objects. IEEE Transactions on Software Engineering. 2003, 29:242-260
[96] V. De Antonellis, M. Melchiori, B. Pernici, et al. A Methodology for e-ServiceSubstitutability in a Virtual District Environment. In: J. Eder, M. Missikoff, eds. Proceedings of the 15th International Conference on Advanced Information Systems Engineering, Klagenfurt, Austria, 2003. Springer, Lecture Notes in Computer Science, 2003, 2681:552-567
[97] V. De Antonellis, M. Melchiori, P. Plebani. An approach to Web service compatibility in cooperative processes. In Proceedings of the 2003 Symposium on Applications and the Internet Workshops, 2003, Washington DC, USA: IEEE Computer Society Press, 2003:95-100
[98] M. Mecella, B. Pernici, P. Craca. Compatibility of e-Services in a Cooperative Multi-platform Environment. Lecture Notes in Computer Science, 2001, 2193:44-57
[99] B.C Pierce. Types and Programming Languages. Massachusetts, USA: The MIT Press, 2002
[100] R. Milner. The Polyadic Pi-Calculus: a Tutorial [Technical Report ECS-LFCS-91-180]. Edinburgh, UK: Laboratory of Foundations of Computer Scienec, Computer Science Department, University of Edinburg, 1991
[101] B. Pierce, D. Sangiorgi. Typing and Subtyping for Mobile Processes. Journal of Mathematical Structures in Computer Science, 1996, 6(5) :409～453
[102] Sangiorgi D, Walker D.The Pi-calculus: a Theory of Mobile Processes.Cambridge: Cambridge University Press, 2001
[103] L.G Meredith., S. Bjorg. Contracts and Types. Communications of the ACM, 2003, 46(10):41-47
[104] S. Gay, M. Hole. Subtyping for session Types in the Pi Calculus. Acta Informatica, 2005, 42(2):192-225
[105] A. Igarashi, N. Kobayashi. A generic type system for the Pi-calculus. Theoretical Computer Science, 2004, 311(1-3):121-163
[106] C. Pahl. A pi-calculus based framework for the composition and replacement of components. In Proceedings of the Workshop on Specification and Verification of Component-Based Systems (OOPSLA 2001), Florida, USA, 2001
[107] A.L Brown, C. Laneve, L.G Meredith. PiDuce: a process calculus with nativeXML datatypes. In: M. Bravetti, L. Kloul, G. Zavattaro, eds. Proceedings of 2005 Workshop on Web Services and Formal Methods, Versailles, France, 2005. Springer, Lecture Notes in Computer Science, 2005, 3670:18-34
[108] L. Acciai, M. Boreale. XPi: a typed process calculus for XML messaging. In: M. Steffen, G. Zavattaro, eds. Proceedings of 7th IFIP International Conference on Formal Methods for Object-Based Distributed Systems (FMOODS), Athens, Greece, 2005. Springer, Lecture Notes in Computer Science, 2005, 3535: 47-66
[109]刘荣胜,黄邵,高鸣春.基于类型化Pi-演算的Web服务组合相容性检测.计算机工程与应用, 2007, 43(7):120-124
[2] M.P Papazoglou. Service-oriented computing: Introduction. Communications of the ACM, 2003, 46(10):24-28
[3] M.P Papazoglou. Service-oriented computing: Concepts, characteristics and directions. In Proceedings of the 4th International Conference on Web Information System Engineering, Roma, Italy, 2003. Washington DC,USA:IEEE Computer Society Press, 2003: 3-10
[4] C. Ferris, J. Farrell. What are Web services? Communications of the ACM, 2003,46(6):31
[5] E. Christensen, F. Curbera, G. Meredith, S. Weerawarana. Web Services Description Language (WSDL) 1.1. http://www.w3.org/TR/2001/NOTE-wsdl-20010315
[6] N. Mitra, Y. Lafon. SOAP Version 1.2 Part 0: Primer (Second Edition). http://www.w3.org/TR/soap12-part0/
[7] L. Clement, A. Hately, C.V. Riegen, T. Rogers. UDDI Version 3.0.2., UDDI Spec Technical Committee Draft.http://uddi.org/pubs/uddi-v3.0.2-20041019.htm
[8] B. Srivastava, J.Koehler. Web Service Composition-Current Solutions and Open Problems. In Proceedings of the 13th International Conference on Automated Planning & Scheduling, Trento, Italy, 2003. California, USA:Advancement of Artificial Intelligence Press, 2003:28-35
[9] D. Beckett, Brian McBride. RDF/XML Syntax Specification (Revised). http://www.w3.org/TR/rdf-syntax-grammar/
[10] D. Martin, M. Burstein, J. Hobbs, O. Lassila, et al. OWL-S: Semantic Markup for Web Services. http://www.w3.org/Submission/OWL-S/
[11] S. McIlraith, T. Son. Adapting Golog for composition of semantic Web services. In: D. Fensel, F. Giunchiglia, D.L. McGuinness, et al, eds. Proceedings of the 8thInternational Conference on Principles of Knowledge Represantation and Reasoning, Toulouse, France, 2002. California, USA:Morgan Kaufmann, 2002:482-493
[12] F. Leymann. Web Services Flow Language (WSFL 1.0). http://xml.coverpages.org/WSFL-Guide-200110.pdf
[13] A. Arkin, S. Askary, S. Fordin, et al. Web Service Choreography Interface (WSCI) 1.0. http://www.w3.org/TR/wsci/
[14] T. Andrews, F. Cubera, H. Dholakia, et al. Business Process Execution Language for Web Services Version1.1.http://www-128.ibm.com/developerworks/library/specification/ws-bpel/
[15] N. Kavantzas, D. Burdett, G. Rizinger, et al. Web Service Choreography Description Language Version 1.0. http://www.w3.org/TR/ws-cdl-10/
[16] A. Arkin. Business Process Modeling Language. http://xml.coverpages.org/BPML-2002.pdf
[17] A. Bucchiarone, S. Gnesi. A Survey on Services Composition Languages and Models. In Proceedings of the International Workshop on Web Services Modeling and Testing, Palermo, Italy, 2006:51-63
[18] R. Dijkman, M. Dumas. Service-oriented Design: A Multi-viewpoint Approach. International Journal of Cooperative Information Systems, 2004, 13(4): 337-368
[19] R. Hull, J.Su.Tools for Composite Web Services: A Short Overview. ACM SIGMOD Record, 2005, 34(2):86-95
[20]岳昆,王晓玲,周傲英. Web服务核心支撑技术:研究综述.软件学报, 2004, 15(3):428-442
[21]饶云,冯博琴,李尊朝.基于Web Services的服务合成技术综述.系统工程与电子技术, 2005, 27(8):1481-1489
[22] W.M.P. van der Aalst, M. Dumas, A.H.M. ter Hofstede. Web Service Composition Languages: Old Wine in New Bottles? Lecture Notes in Computer Science, 2003, 2593:59-72
[23] J.C.M Baeten. A brief history of process algebra. Theoretical Computer Science, 2005, 335(2-3):131-146
[24] R.Hamadi, B.Benatallah. A Petri Net-based Model for Web Service Composition. In: K. Schewe, Xiaofang Zhou, eds. Proceedings of 14th Australasian DatabaseConference on Database Technologies, Adelaide, Australia, 2003. Australian Computer Society: 2003(17):191-200
[25] W.M.P van der Aalst, A.H.M. ter Hofstede. Verification of Workflow Task Structures: A Petri-Net-Based Approach. Information Systems, 2000, 25(1):43-69.
[26] W.M.P van der Aalst. Woflan: A Petri-net-based Workflow Analyzer. Systems Analysis, Modeling, Simulation, 1999, 35(3):345-357.
[27] H.M.W. Verbeek, T. Basten, W.M.P. van der Aalst. Diagnosing workow processes using Woan. The Computer Journal, 2001, 44(4):246-279
[28] D.Berardi, D.Calvanese, G. De Giacomo,et al. Automatic Composition of e-Services that Export their Behavior. Lecture Notes in Computer Science, 2003, 2910:43-58
[29] D.Berardi, D.Calvanese, G. De Giacomo,et al. Automatic Services Composition based on Behavior Descriptions. International Journal of Cooperative Information Systems, 2005, 14(4):333-376
[30] D.Berardi, G. De Giacomo, M. Lenzerini, et al. Synthesis of underspecified composite e-services based on automated reasoning. In:M. Aiello, M. Aoyama, F. Curbera, et al, eds. Proceedings of 2th International Conference on Service-Oriented Computing, New York, USA, 2004. ACM Press, 2004:105-114
[31] G. De Giacomo, M. Lenzerini. PDL-based framework for reasoning about actions. Lecture Notes in Artificial Intelligence, 1995, 992:103-114
[32] J.E. Hopcroft, R. Motwani, J.D. Ullman. Introduction to Automata Theory, Languages, and Computation (2nd Edition). Boston,USA:Addison Wesley, 2000
[33] T.Bultan, X.Fu, R.Hull, J.Su. Conversation Specfication: A new approach to design and analysis of e-service composition. In Proceedings of 12th International Conference on World Wide Web, Budapest, Hungary, 2003. ACM Press, 2003:403-410
[34] X.Fu, T.Bultan, J.Su. Conversation protocols: A formalism for specification and verification of reactive electronic services. In: O.H. Ibarra, Zhe Dang, eds. Proceedings of 8th International Conference on Implementation and Application of Automata, California, USA, 2003. Spinger, Lecture Notes in Computer Science, 2003,2759:188-200
[35] G. Plotkin. Call-by-name, call-by-value, and theλ-Calculus. Theoretical Computer Science, 1975, 1:125-159
[36] C.A.R Hoare. Communicating Sequential Processed. Commucation of the ACM. 1978,21(8):666-677
[37] C.A.R. Hoare. Communicating Sequential Processes. New Jersey,USA: Prentice-Hall, 1985
[38] R. Milner. A Calculus of Communicating Systems. Lecture Notes in Computer Science, 1980, Volume 92
[39] R. Milner, J.Parrow, D. Walker. A calculus of mobile process (PartsⅠandⅡ). Information and Computation, 1992, 100:1-77
[40] R. Milner. Communicating and Mobile Systems: The Pi Calculus. Cambridge: Cambridge University Press, 1999.
[41] T. Bolognesi, E. Brinksma. Introduction to the ISO Specification Language LOTOS. Computer Network and ISDN Systems, 1987, 14:25-59
[42] G. Salaün, L. Bordeaux, M. Schaerf. Describing and Reasoning on Web Services using Process Algebra. In Proceedings of the 2th IEEE International Conference on Web Services, California, USA, 2004. Washington DC,USA:IEEE Computer Society Press, 2004:43-50
[43] S. Schneider, J. Davis, D.M. Jackson, et al. Timed CSP: Theory and Practice. Lecture Notes in Computer Science, 1992, 600:640-675
[44] A. Ferrara. Web services: a process algebra approach. In: M. Aiello, M. Aoyama, F. Curbera, et al, eds. Proceedings of 2th International Conference on Service Oriented Computing, New York, USA, 2004. ACM Press, 2004: 242-251
[45] G. Salaün, A. Ferrara, and A. Chirichiello. Negotiation among web services using LOTOS/CADP. Lecture Notes in Computer Science, 2004, 3250:198-212
[46] L. Bordeaux and G. Salaün. Using process algebra for web services: Early resultsand perspectives. Lecture Notes in Computer Science, 2004, 3324:54-68
[47] A. Brogi, C. Cannl, E. Pimentel. Formalizing Web Service Choreographies. ElectronicNotes in Theoretical Computer Science, 2004, 105: 73-94
[48] H. Foster, S. Uchitel, J. Magee, et al. Model based verification of web service compositions. In Proceedings of 18th International Conference on Automated Software Engineering, Montreal, Canada, 2003.Washington DC,USA:IEEE Computer Society Press, 2003: 152-163
[49] H. Foster, S. Uchitel, J. Kramer, et al. Compatibility verification for web service choreography. In Proceedings of the 2th International Conference on Web Services, California, USA, 2004. Washington DC, USA:IEEE Computer Society Press, 2004:738-741
[50] H. Foster, S. Uchitel, J. Magee, et al. Using a rigorous approach for engineering web service compositions: a case study. In Proceedings of the 2005 IEEE International Conference on Services Computing, Orlando, USA, 2005. Washington DC, USA: IEEE Computer Society Press, 2005, 1: 217-224.
[51] H. Foster, S. Uchitel, J. Magee,et al. Model-Based analysis of Obligations in Web Service Choreography. In Proceedings of the Advanced International Conference on Telecommunications and International Conference on Internet and Web Applications and Services, Guadeloupe, French, 2006. Washington DC, USA: IEEE Computer Society Press, 2006:149-157
[52] M. Koshkina, F. van Breugel. Modelling and verifying web service orchestration by means of the concurrency workbench. ACM SIGSOFT Software Engineering Notes, 2004, 29(5):1-10
[53] M. Koshkina. Verification of business processes for web services [Master's thesis]. Toronto, Canada:York University, 2003
[54] M. Viroli. Towards a formal foundation to orchestration languages. In Proceedings of the first International Workshop on Web Services and Formal Method, Pisa, Italy, 2004. Elsevier, Electronic Notes in Theoretical Computer Science, 2004, 15:51-71
[55] E. Oren, A. Haller. Formal Frameworks for Workflow Modelling [DERI Technical Report 2005-4-07]. Galway, Ireland: Digital Enterprise Research Institude, National University of Ireland, 2005
[56] F. Puhlmann. Why do we actually need the Pi-Calculus for Business Process Management? In:W. Abramowicz, H.C. Mayr, eds. Proceedings of 9th International Conference on Business Information Systems (BIS 2006), Klagenfurt, Austria, 2006. Lecture Notes in Informatics, 2006, 85: 77-89
[57] F. Puhlmann, M. Weske. Using the Pi-Calculus for Formalizing Workflow Patterns. In Proceedings of 3th International Conference on Business Process Management , Nancy, France, 2005: 153-168
[58] H. Overdick, F. Puhlmann,M. Weske. Towards a Formal Model for Agile Service Discovery and Integration. In Proceedings of first International ICSOC Workshop on Dynamic Web Processes (ICSOC-DWP05), Amsterdam, Netherlands, 2005
[59] S.J. Woodman, D.J. Palmer, S.K. Shrivastava, et al. Notations for the Specification and Verification of Composite Web Services. In Proceedings of the 8th IEEE International Enterprise Distributed Object Computing Conference., California, USA, 2004. Washington DC,USA:IEEE Computer Society Press, 2004:35-46
[60] J. Camara, C. Canal, J.Cubo. Issues in the formalization of Web Service Orchestrations. In Proceedings of 2th International Workshop on Coordination and Application Techniques for Software Entities, Glasgow, Scotland, 2005:17-24
[61] Y. Yang, Q. Tan, and Y. Xiao. Verifying web services composition. Lecture Notes in Computer Science, 2005, 3770: 354-363
[62] Y. Yang, Q. Tan, and Y. Xiao. Verifying web services composition based on hierarchical colored Petri nets. In:A. Hahn, S. Abels, L. Haak, eds. Proceedings of the first International ACM Workshop on Interoperability of Heterogeneous Information Systems, Bremen, Germany, 2005. ACM Press, 2005: 47-54
[63] Yang, Q. Tan, Y. Xiao, J. Yu, and F. Liu. Exploiting hierarchical CP-nets to increase reliability of web services workflow. In Proceeding of the International Symposium on Applications and the Internet, Phoeniz, AZ, USA, 2006. Washington DC, USA:IEEE Computer Society Press, 2006:116-122
[64]张文涛,彭泳,陈俊亮.基于Petri网的Web服务自动组合研究.计算机学报, 2006, 29(7):1058-1066
[65]张文涛,彭泳,陈俊亮.会话类E-Service的接口兼容和服务组合分析.计算机学报, 2006, 29(7):1047-1056
[66]杨鑫,陈俊亮. WSC/ADL:Web服务组合系统体系结构描述语言.软件学报, 2006, 17(5):1182-1194
[67]陈彦萍,李增智,唐亚哲等.一种满足马尔可夫性质的不完全信息下的Web服务组合方法.计算机学报, 2006, 29(7):1167-1178
[68]陈彦萍,李增智,郭志胜. Web服务组合中基于服务质量的服务选择算法.西安交通大学学报, 2006, 40(8):897-905
[69]漆玉松,钱柱中,是湘全.基于Agent的Web服务组合研究.南京理工大学学报, 2006, 30(3):315-319
[70]廖军,谭浩,刘锦德.基于Pi-演算的Web服务组合的描述和验证.计算机学报, 2005, 28(4):635-643
[71] J.C.M Baeten, W.P. Weijand. Process Algebra. Cambridge Tracts in Theoretiacl Computer Science, volume 18. Cambridge, England:Cambridge University Press, 1990
[72] G. Winskel. The Formal Semantics of Programming Languages: An Introduction. Massachusetts, USA: The MIT Press, 1993
[73] G. Plotkin. A structural approach to operational semantics [Technical Report DAIMI FN-19], Aarhus, Denmark: Computer Science Department, Aarhus University, 1981.
[74] D.Turi, G.Plotkin. Towards a Mathematical Operational Semantics. In Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, 1997. Washington DC, USA:IEEE Computer Society Press, 1997:280-291
[75] R.D Tennent. The denotaional semantics of programming languages. Communication of the ACM, 1976, 19(8):437-453
[76] S. Owicki, D. Gries, Verifying properties of parallel programs: an axiomatic approach, Communications of the ACM, 1976, 19(5):279-285
[77] P. Wohed, W.M.P van de Aalst, M. Dumas, et al. Pattern Based Analysis of BPEL4WS [FIT-TR-2002-04 Technical Report]. Queensland, Australia:Queensland University of Technology, 2003
[78] D. SANGIORGI. A Theory of Bisimulation for the pi-Calculus. Acta Informatica, 1996, 3(1): 69-97
[79] M.Hennessy, H. Lin. Symbolic bisimulations, Theoretical Computer Science, 1995, 138(2): 353-369
[80] Yuxi Fu. Bisimulation congruence of Pi-calculus, Information and Computation, 2003, 184(1):201-226
[81] B. Victor. A Verification Tool for the Polyadic Pi-Calculus [DoCS Licentiate thesis 94/50]. Uppsala, Sweden: Department of Computer Systems, Uppsala University, 1994
[82] B. Victor, F. Moller. The Mobility Workbench-A Tool for the Pi-Calculus. In: D.Dill, ed. Proceedings of the 6th International Conference on Computer Aided Verification, California, USA, 1994. Springer, Lecture Notes in Computer Science, 1994, 818:428-440
[83] M. Dam. Model Checking Mobile Processes. Lecture Notes in Computer Science, 1993, 715:22-36
[84] A. Barros, M. Dumas, P. Oaks. A Critical Overview of the Web Services Choreography Description Language (WS-CDL). Business Process Trends, 2005. http://www.bptrends.com
[85] J. Mendling, M. Hafner. From WS-CDL Choreography to BPEL Process Orchestration. http://wi.wu-wien.ac.at/home/mendling/publications/TR06-CDL.pdf
[86] N. Busi, R. Gorrieri, C. Guidi, et al. Towards a formal framework for Choreography. In Proceedings of the 14th IEEE International Workshops on Enabling Technologies: Infrastructures for Collaborative Enterprises (WETICE-2005), Linkoping, Sweden, 2005. Washington DC,USA:IEEE Computer Society Press, 2005: 107-112
[87] R. Gorrieri, C. Guidi, R. Lucci. Reasoning about interaction patterns in Choreography. In: M. Bravetti, L. Kloul, G. Zavattaro, eds. Proceedings of 2th International Workshop on Web Services and Formal Methods (WS-FM '05), Versailles, France, 2005. Springer, Lecture Notes in Computer Science, 2005, 3670:333-348
[88] W.L Yeung, J. Wang, W. Dong. Verifying Choreographic Descriptions of WebServices Based on CSP. In Proceedings of the IEEE Services Computing Workshops (SCW'06), 2006. Washington DC,USA:IEEE Computer Society Press, 2006:97-104
[89] M. Baldoni, C. Baroglio, A. Martelli, et al. Verifying the Conformance of Web Services to Global Interaction Protocols: A First Step. In Proceedings of the 2th International WorkShop on Web Services and Formal Methods, Versailles, France, 2005. Springer, Lecture Notes in Computer Science, 2005, 3670:257-271
[90] Xiangpeng Zhao, Hongli Yang, Zongyan Qiu. Towards the Formal Model and Verification of Web Service Choreography Description Language. In: M. Bravetti, M. Nú?ez, G. Zavattaro, eds. Proceedings of the 3th International Workshop on Web Service and Formal Methods, Vienna, Austria, 2006. Springer, Lecture Notes in Computer Science, 2006, 4184:273-287
[91] L.Bordeaux, G.Salaün, D.Berardi, et al. When are two Web Services Compatible? In: Ming-Chien Shan, U.Dayal, M. Hsu, eds. Proceedings of the 5th International Workshop on Technologies for E-Services, Toronto, Canada, 2004. Springer, Lecture Notes in Computer Science, 2004, 3324:15-28
[92] Yuliang Shi, Liang Zhang, Fangfang Liu, et al. Compatibility Analysis of Web Services. In: A. Skowron, R. Agrawal, M. Luck, et al, eds. Proceedings of the 2005 IEEE/WIC/ACM International Conference on Web Intelligence, Compiěgne, France, 2005. Washington DC,USA:IEEE Computer Society Press, 2005:483-486
[93] Fangfang Liu, Liang Zhang, Yuliang Shi, et al. Formal analysis of Compotibility of Web Services via CCS. In Proceedings of the International Conference on Next Generation Web Services Practices, Seoul, Korea, 2005. Washington DC, USA: IEEE Computer Society Press, 2005:143-148
[94] YunYao Li, H.V. Jagadish. Compatibility Determiation in Web Services. In Proceedings of the first International E-Services Workshop, Pittsburgh, USA, 2003:7-15
[95] C.Canal, L.Fuentes, E.Pimentel, et al. Adding Roles to CORBA Objects. IEEE Transactions on Software Engineering. 2003, 29:242-260
[96] V. De Antonellis, M. Melchiori, B. Pernici, et al. A Methodology for e-ServiceSubstitutability in a Virtual District Environment. In: J. Eder, M. Missikoff, eds. Proceedings of the 15th International Conference on Advanced Information Systems Engineering, Klagenfurt, Austria, 2003. Springer, Lecture Notes in Computer Science, 2003, 2681:552-567
[97] V. De Antonellis, M. Melchiori, P. Plebani. An approach to Web service compatibility in cooperative processes. In Proceedings of the 2003 Symposium on Applications and the Internet Workshops, 2003, Washington DC, USA: IEEE Computer Society Press, 2003:95-100
[98] M. Mecella, B. Pernici, P. Craca. Compatibility of e-Services in a Cooperative Multi-platform Environment. Lecture Notes in Computer Science, 2001, 2193:44-57
[99] B.C Pierce. Types and Programming Languages. Massachusetts, USA: The MIT Press, 2002
[100] R. Milner. The Polyadic Pi-Calculus: a Tutorial [Technical Report ECS-LFCS-91-180]. Edinburgh, UK: Laboratory of Foundations of Computer Scienec, Computer Science Department, University of Edinburg, 1991
[101] B. Pierce, D. Sangiorgi. Typing and Subtyping for Mobile Processes. Journal of Mathematical Structures in Computer Science, 1996, 6(5) :409～453
[102] Sangiorgi D, Walker D.The Pi-calculus: a Theory of Mobile Processes.Cambridge: Cambridge University Press, 2001
[103] L.G Meredith., S. Bjorg. Contracts and Types. Communications of the ACM, 2003, 46(10):41-47
[104] S. Gay, M. Hole. Subtyping for session Types in the Pi Calculus. Acta Informatica, 2005, 42(2):192-225
[105] A. Igarashi, N. Kobayashi. A generic type system for the Pi-calculus. Theoretical Computer Science, 2004, 311(1-3):121-163
[106] C. Pahl. A pi-calculus based framework for the composition and replacement of components. In Proceedings of the Workshop on Specification and Verification of Component-Based Systems (OOPSLA 2001), Florida, USA, 2001
[107] A.L Brown, C. Laneve, L.G Meredith. PiDuce: a process calculus with nativeXML datatypes. In: M. Bravetti, L. Kloul, G. Zavattaro, eds. Proceedings of 2005 Workshop on Web Services and Formal Methods, Versailles, France, 2005. Springer, Lecture Notes in Computer Science, 2005, 3670:18-34
[108] L. Acciai, M. Boreale. XPi: a typed process calculus for XML messaging. In: M. Steffen, G. Zavattaro, eds. Proceedings of 7th IFIP International Conference on Formal Methods for Object-Based Distributed Systems (FMOODS), Athens, Greece, 2005. Springer, Lecture Notes in Computer Science, 2005, 3535: 47-66
[109]刘荣胜,黄邵,高鸣春.基于类型化Pi-演算的Web服务组合相容性检测.计算机工程与应用, 2007, 43(7):120-124