Web服务组合形式化建模与验证研究
|
摘要
面向服务的体系结构SOA (Service-Oriented Architeture)是一种新的分布式应用程序体系结构,它是构件重用和分布式技术发展的结果,业界提出将面向服务的体系结构作为软件体系结构下一个发展阶段来帮助IT组织应对所面临的越来越多的复杂性挑战。Web服务(Web Services)是当前实现SOA范型最有前景的技术。Web服务技术的广泛应用使得Web服务正逐步成为Internet网络环境中资源封装的标准形式。随着部署在Internet上的Web服务不断丰富,这些可被公共访问和集成的服务构成了一个潜在的巨大标准组件库。在Web服务互操作技术的基础上,提供高层的Web服务集成手段、实现Web服务组合成为Web服务技术发展的自然需求。总结当前的Web服务组合建模方法,主要分为语法方法、语义方法和形式化方法等。相对于其他服务组合方法,形式化建模方法有不可替代的重要作用。本论文从理论研究和实践结合两个方面着手,探索服务组合的形式化建模和验证技术。本论文的主要工作如下：
1.建立了Web服务组合形式化模型,重点研究了用于描述Web服务交互过程的服务交互过程模型
Web服务组合模型FMWSC (Formal Model for Web Service Composition)由两部分组成：服务描述模型、以及服务交互过程模型。服务描述模型基于Web服务描述语言WSDL (Web Services Description Language),用于描述Web服务组合的静态信息；服务交互过程模型用于描述Web服务的交互过程。Web服务交互过程模型能清晰表达Web服务组合中各组成部分之间的交互,并可模拟Web服务的交互过程,分析其动态性质。
2.为了保证服务交互过程的正确性,给出了服务交互过程的形式化验证方法
服务交互过程的形式化验证方法将模块化思想与模型验证技术相结合,即在对服务交互过程进行形式化验证时,重点验证服务基本交互过程。服务交互全过程的性质由这些基本过程的性质以及这些基本过程的组合方式所决定。采用这种方法的好处是可以有效地降低系统验证的规模,并提高验证的效率。验证的基本思路是：首先应用IMWSC模型的语义转换函数,将IMWSC描述转换为通信系统演算CCS表示,然后利用CWB-NC工具提供基于模态逻辑的检测机制对IMWSC模型实例进行验证。
3.应用FMWSC建立了车辆维修管理系统模型,并应用本文提出的服务交互过程的验证机制对该系统的主要属性和行为一致性进行了验证
以一个车辆维修管理系统VRMS (Vehicle Repair Management System)为例,详细介绍服务组合模型FMWSC的实际应用。首先给出组成VRMS系统的服务组件的静态描述,然后应用服务交互过程模型给出了(组成VRMS系统的)服务间的交互过程描述,并应用本文给出的服务交互过程模型的验证机制对该系统的主要属性和行为一致性进行了实际验证。在介绍CCML (Cooperative Computation Modeling Language)语言的基础上,给出了FMWSC模型与CCML语言的对应关系,并给出VRMS系统的(部分)CCML代码。
Recently, Service-Oriented Archtecutre (SOA in short) has drawn a lot of attention. It is a kind of new distributed application architecture and component technology. SOA which can help IT organizations meet more challenging requirement of market is promoted in the industry as the next evolutionary step in software architecture. Web services are the most promising technique to realze SOA. Web services are software applications which can be used through a network (intranet or Internet) via the exchange of messages based on XML standards. Due to the limit of the function that a single web service can provide, web services usually need to be composed into larger ones to meet the users' requirement. Composition approaches for web services can be generally divided into three groups:the workflow based methods, the ontology based methods and the formal methods.
This paper aims to study the formal method of modeling and analyzing the compositon of web services. The main contribution of this paper is introduced as following:
1. The Development of Web Service Composition Model FMWSC
Web service compositon model FMWSC (Formal Model for Web Service Composition) comprised two parts:Service Description Model and Service Interaction Model. Service Description Model is based on WSDL (Web Services Description Language) and used for describing the stactic information of web service composition; Service Interaction Model is used for describing the dynamic information of web services.
2. The Development of the Formal Verification Method for Determing the Properties and Correctness of the Service Interaction Process
The formal verification method for the Service Interaction Model focuses on verifying the properties of the basic interaction processes. The properties of the complete service interaction process are determined by the properties of the basic interaction process and the way these basic processes are composed. A distingusing merit of our method is the scale of the model checking can be reduced, and therefore the efficiency of model checking can be improved. The semantics of IMWSC is studied. This semantics comprised three parts:semantic domain, semantic range, and the valuation functions. Based on the semantics of MWSC, the formal verification method of IMWSC is given. A kind of modal logic,μ-calculus is introduced as the formal reasoning logic to verify the properties of IMWSC Instances.
3. Investigating the Application of the FMWSC Model on a Case Study
The application of the FMWSC Model is further investigated in a Vehicle Repair Management System (VRMS). First step is describing the the stactic information of the components that compose the VRMS system. The second step is describing the interactive process of these components by using the Service Interaction Model. Then the prime properties of the system and the behavior consistency are verified. Finally, after introducing the web service composition execution language CCML (Cooperative Computation Modeling Language) and the correspondence relation between FMWSC and CCML, (part of) the CCML code of VRMS system was given.
1.建立了Web服务组合形式化模型,重点研究了用于描述Web服务交互过程的服务交互过程模型
Web服务组合模型FMWSC (Formal Model for Web Service Composition)由两部分组成：服务描述模型、以及服务交互过程模型。服务描述模型基于Web服务描述语言WSDL (Web Services Description Language),用于描述Web服务组合的静态信息；服务交互过程模型用于描述Web服务的交互过程。Web服务交互过程模型能清晰表达Web服务组合中各组成部分之间的交互,并可模拟Web服务的交互过程,分析其动态性质。
2.为了保证服务交互过程的正确性,给出了服务交互过程的形式化验证方法
服务交互过程的形式化验证方法将模块化思想与模型验证技术相结合,即在对服务交互过程进行形式化验证时,重点验证服务基本交互过程。服务交互全过程的性质由这些基本过程的性质以及这些基本过程的组合方式所决定。采用这种方法的好处是可以有效地降低系统验证的规模,并提高验证的效率。验证的基本思路是：首先应用IMWSC模型的语义转换函数,将IMWSC描述转换为通信系统演算CCS表示,然后利用CWB-NC工具提供基于模态逻辑的检测机制对IMWSC模型实例进行验证。
3.应用FMWSC建立了车辆维修管理系统模型,并应用本文提出的服务交互过程的验证机制对该系统的主要属性和行为一致性进行了验证
以一个车辆维修管理系统VRMS (Vehicle Repair Management System)为例,详细介绍服务组合模型FMWSC的实际应用。首先给出组成VRMS系统的服务组件的静态描述,然后应用服务交互过程模型给出了(组成VRMS系统的)服务间的交互过程描述,并应用本文给出的服务交互过程模型的验证机制对该系统的主要属性和行为一致性进行了实际验证。在介绍CCML (Cooperative Computation Modeling Language)语言的基础上,给出了FMWSC模型与CCML语言的对应关系,并给出VRMS系统的(部分)CCML代码。
Recently, Service-Oriented Archtecutre (SOA in short) has drawn a lot of attention. It is a kind of new distributed application architecture and component technology. SOA which can help IT organizations meet more challenging requirement of market is promoted in the industry as the next evolutionary step in software architecture. Web services are the most promising technique to realze SOA. Web services are software applications which can be used through a network (intranet or Internet) via the exchange of messages based on XML standards. Due to the limit of the function that a single web service can provide, web services usually need to be composed into larger ones to meet the users' requirement. Composition approaches for web services can be generally divided into three groups:the workflow based methods, the ontology based methods and the formal methods.
This paper aims to study the formal method of modeling and analyzing the compositon of web services. The main contribution of this paper is introduced as following:
1. The Development of Web Service Composition Model FMWSC
Web service compositon model FMWSC (Formal Model for Web Service Composition) comprised two parts:Service Description Model and Service Interaction Model. Service Description Model is based on WSDL (Web Services Description Language) and used for describing the stactic information of web service composition; Service Interaction Model is used for describing the dynamic information of web services.
2. The Development of the Formal Verification Method for Determing the Properties and Correctness of the Service Interaction Process
The formal verification method for the Service Interaction Model focuses on verifying the properties of the basic interaction processes. The properties of the complete service interaction process are determined by the properties of the basic interaction process and the way these basic processes are composed. A distingusing merit of our method is the scale of the model checking can be reduced, and therefore the efficiency of model checking can be improved. The semantics of IMWSC is studied. This semantics comprised three parts:semantic domain, semantic range, and the valuation functions. Based on the semantics of MWSC, the formal verification method of IMWSC is given. A kind of modal logic,μ-calculus is introduced as the formal reasoning logic to verify the properties of IMWSC Instances.
3. Investigating the Application of the FMWSC Model on a Case Study
The application of the FMWSC Model is further investigated in a Vehicle Repair Management System (VRMS). First step is describing the the stactic information of the components that compose the VRMS system. The second step is describing the interactive process of these components by using the Service Interaction Model. Then the prime properties of the system and the behavior consistency are verified. Finally, after introducing the web service composition execution language CCML (Cooperative Computation Modeling Language) and the correspondence relation between FMWSC and CCML, (part of) the CCML code of VRMS system was given.
引文
[1]F. Curbera, R. Khalaf, N. Mukhi, et al. The next step in web services. Communications of the ACM, 2003,46(10):29-34.
[2]Mark Endrei, Jenny Ang, Ali Arsanjani, et al. Patterns:Service-Oriented Architecture and Web Services. IBM Technical Report. Available at: http://www.redbooks.ibm.com/redbooks/pdfs/sg246303.pdf.
[3]邓水光,李荧,吴健.Web服务行为兼容性的判定与计算.软件学报,2007,18(12)：3001-3014.
[4]Kramer L, Salaun G, Berardi D, Mecella M. When Are Two Web Services Compatible. In:Proc. of the 5th VLDB International Workshop on Technologies for e-Services (VLDB-TES),2004.
[5]Foster H, Uchitel S, Magee J, et al. Compatibility verification for web service choreography. In:Proc. of International Conference on Web Service (ICWS),2004.
[6]Wombacher A, Fankhauser P, Mahleko B, et al. Matchmaking for Business Processes based on Choreographies. International Journal of Web Services Research,2004,1(4):14-32.
[7]X. Fu, T. Bultan, J. Su. Analysis of Interacting BPEL Web Services. In:Proc. of 13th Int. Conf. World Wide Web (WWW), ACM Press,2004:621-630.
[8]Martens A. On compatibility of web services. Petri Net Newsletter.2003,65:12-20.
[9]H. Foster, S. Uchitel, J. Kramer, et al. Compatibility verification for web service choreography. In:Proc. of the 2th International Conference on Web Services,2004:738-741.
[10]H. Foster, S. Uchitel, J. Magee, et al. Model-based verification of web service compositions. In:Proc. of 18th IEEE International Conference on Automated Software Engineering,2003:152-163.
[11]H. Foster, S. Uchitel, J. Magee, et al. LTSA-WS:A Tool for Model-based Verification of Web Service Compositions and Choreography. In:Proc. of ICSE 2006:771-774.
[12]岳昆,于晓玲,周傲英.Web服务核心支撑技术：研究综述.软件学报,2004,15(3)：428-442.
[13]饶云,冯博琴,李尊朝.基于Web Services的服务合成技术综述.系统工程与电子技术,2005,27(8)：1481-1489
[14]G. J. Holzmann. The Spin Model Checher: Primer and Reference Manual. Boston:Addison-Wesley, 2004.
[15]冯名正.Web服务组合研究综述.计算机应用与软件,2007,24(2)：23-27.
[16]J. Misra, W. Cook. Computing Orchestration:A Basis for Wide-Area Computing. Journal of Software & Systems Modeling,2007,6(1):83-110.
[17]Nickolas Kavantzas, David Burdett, Gregory Ritzinge, et al. Web Services Choreography Description Language Version 1.0. W3C Working Draft.Available at: http://www.w3.org/TR/2004/WD-ws-cdl-10-20041217/.
[18]G. Diaz, J.J. Pardo, M.-E. et al. Automatic Translation of WS-CDL Choreographies to Timed Automata. In:Proc. of Int. Workshop on Web Services and Formal Methods (WS-FM2005), Springer, 2005:230-242.
[19]Tao X. F., Jiang C. J.. Formalizing Web service and modeling Web service based system based on object oriented Petri net. Lecture Notes in Computer Science. Berlin:Springer-Verlag,2004: 1008-1011.
[20]郭玉彬,杜玉越,系建清.Web服务组合的有色网模型及运算性质.计算机学报,2006,29(7)：1067-1075.
[21]X. Yi, K.J. Kochut. A CP-nets-based design and verification framework for web services composition. In:Proc. of the 2nd IEEE International Conference on Web Services,2004:756-760.
[22]K. Schmidt, C. Stahl. A Petri net semantic for BPEL4WS-validation and application. In:Proc. of the 11 the Workshop on Algorithms and Tools for Petri Nets,2004:1-6.
[23]Zhang Jia, Chung Jen Yao, Chang C. K., Kim S.. WS-Net:A petri-net based specification model for web service. In:Proc. of the 2nd IEEE International Conference on Web Services,2004:420-427.
[24]R.Hamadi, B.Benatallah. A Petri Net-based Model for Web Service Composition. In:Proc. of the 14th Australasian Database Conference on Database Technologies,2003: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 Wolfan. The Computer Journal,2001,44(4):246-279.
[28]M. Baldoni, C. Baroglio, A. Martelli, et al. Verifying the conformance of web services to global interaction protocols:a first step. In Proc of the 2nd International Workshop on Web Services and Formal Methods, Versailles:Lecture Notes in Computer Science,2005:257-271.
[29]肖美华,薛锦云.时态逻辑形式化描述并发系统性质.海军工程大学学报,2004,16(5)：10-13.
[30]辜希武.Web服务组合形式化模型研究：(博士学位论文),武汉：华中科技大学,2007.
[31]周永华,陆化普.基于Web服务的智能交通系统集成.计算机工程,2006,32(8)：244-246.
[32]J. E. Hopcroft, R. Motwani, J. D. Ullman. Introduction to Automata. Theory, Languages, and Computation (2nd Edition).Boston: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 Proc. of 12th International Conference on World Wide Web, Budapest: 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. Proc. of 8th International Conference on Implementation and Application of Automata,California:Lecture Notes in Computer Science,2003, 2759:188-200.
[35]G.Plotkin. Call-by-name, call-by-value, and the A,-Calculus. Theoretical Compute Science,1975,1: 125-159.
[36]付燕宁.Web服务组合方法研究：(博士学位论文),长春：吉林大学,2007.
[37]C.A.R.Hoare. Communicating Sequential Processes. New Jersey:Prentice-Hall,1985.
[38]Mads Dam. CCS:Processes and Equivalences. Technical Report. Available at: http://www.imit.kth.se/courses/2G1516/Docs05/Slides/CCS-lecture-1.5.pdf.
[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.Salaun, L.Bordeaux, M.Schaerf. Describing and Reasoning on Web Service using Process Algebra.In Proc. of the 2th IEEE International Conference on Web Services, California:IEEE Computer Society Press,2004:43-50.
[43]金仙力.实时服务构件的语义特征和行为组装形式化技术研究：(博士学位论文),北京：北京邮电大学,2008.
[44]A.Ferrara. Web services:a process algebra approach. In:M.Aiello, M.Aoyama, FCurbera, et al, eds. Proc. of 2th International Conference on Service Oriented Computing, New York, USA,2004. ACM Press,2004:242-251
[45]Rance Cleaveland, Tan Li, Steve Sims. The Concurrence Workbench of the New Century. User's Manual. Available at:http://www.cs.sunysb.edu/-cwb/.
[46]杨涛,刘锦德.Web Services技术综述—一种面向服务的分布式计算模式.计算机应用,24(8)：1-4.
[47]M. Butler, C. Ferreira, M.Y.Ng. Precise modeling of compensating business transactions and its applications to BPEL. Jounal of Universal Computer Science,2005,11(5):712-743.
[48]Van der Aalst WMP. The Application of Workflow Management[J]. Journal of Circuits, Systems and Computers,1998,8(1):21-66.
[49]B. F Chellas. Modal Logic:An Introduction. Cambridge University Press,1980.
[50]M. H. ter Beek, A. Bucchiarone, S. Gnesi. Formal Methods for Serivce Composition. Technical Report. Software/Program Verification, Formal Methods, ACM.
[51]M. H. ter Beek, A. Bucchiarone, S. Gnesi. A Survey on Serivce Composition Approaches:From Industrial Standards to Forml Methods. Technical Report. Software/Program Verification, Formal Methods, ACM.
[52]阎志华,丁秋林.基于Petri网的Web服务流程建模.计算机应用,23(12)：55-57.
[53]Bucchiarone, Gnesi. A Survey on Serivce Composition Language and Models. In:Proc. of International Workshop on Web Service Modeling and Testing,2006:51-63.
[54]E. A. Emerson, C. L. Lei. Efficient model checking in fragments of the propositional mu-calculus. In: Proc. of the Symposium on Logic in Computer Science (LISC'86), Cambrige:IEEE Computer Society Press,1986:267-278
[55]Jensen K.. Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Volume 1, Basic Concepts, Monographs in Theoretical Computer Science. Springer-Verlag,1997.
[56]Luca Aceto, Kim G. Larsen. An Introduction to Milner's CCS. Technical Report, Department of Computer Science, Aalborg University, Aalborg, Denmark, March 2005. Available at: http://www.dimi.uniud.it/miculan/Didattica/MFGC04/intro2ccs.pdf.
[57]Leslie Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering,1977,3(2):125-143.
[58]葛声,马殿富,胡春明.基于Web服务的网络软件运行平台研究与实现.北京航空航天大学学报,2003,29(10)：897-900.
[59]Beard B, Bidoit M, Finkel. System and Software Verification:Model Checking Techniques and Tools. Berlin:Springer-Verlag,2001.
[60]Wil van der Aalst, Kees van Hee工作流管理-模型、方法和系统.北京：清华大学出版社,2004.
[61]Emerson E A, Haopen J Y. "Sometimes" and "Not Never" revised:on branching versus Linear time temporal logic [J]. Journal of the ACM,1986,9(1):12-17.
[62]廖军.面向服务计算(SOC)中服务组合的研究：(博士学位论文),武汉：华中科技大学,2007.
[63]倪晚成,刘连臣,吴澄.Web服务组合方法综述.计算机工程,2008,32(4)：79-81.
[64]蒋哲远,韩江洪,王钊.动态的QoS感知Web服务选择和组合优化模型.计算机学报,2006,32(5)：1015-1025.
[65]黄小庆,夏安邦.基于有色Petri网和分类服务的Web服务组合模型.计算机集成制造系统.2009,15(1)：53-62.
[66]周相兵,杨小平,向昌成,谢成锦.面向本体的语义服务组合评价模型研究.计算机集成制造系统,2008,14(12)：2346-2353.
[67]陈彦萍,李增智,唐亚哲.一种满足马尔可夫性质的不完全信息下的Web服务组合方法.计算机学报,2006,29(7)：1167-1178.
[68]陈彦萍,李增智,郭志胜.Web服务组合中基于服务质量的服务选择算法.西安交通大学学报,2006,40(8)：897-905.
[69]李喜彤,范玉顺.Web服务过程建模及其逻辑正确性验证.计算机集成制造系统,2008,14(4)：675-682.
[70]廖军,谭浩,刘锦德.基于Pi-演算的Web服务组合的描述和验证.计算机学报,2005,28(4)：635-643.
[71]Biplav Srivastava, Jana Koehler. Web Service Composition:Current Solutions and Open Problems. In: In:Proc. of the 13th International Conference on Automated Planning & Scheduling (ICAPS 2003), Workshop on Planning for Web Services,2003:28-35.
[72]高勇,刘瑜.一个基于Petri网的Web服务组合模型.计算机工程,32(6),2006：17-19.
[73]张秀国.基于过程网络的服务协同计算模型研究：(博士学位论文),大连：大连海事大学,2006.
[74]Li Bao, Weishi Zhang, Xiuguo Zhang. Describing and Verifying Web Service Using CCS. In:Proc. of the 7th International Conference on Parallel and Distributed Computing, Applications and Technologies,2006.
[75]R. Cleaveland and S. Sims. The NCSU concurrency workbench. In R. Alur and T. Henzinger, editors, Proc. of the 8th International Conference on Computer Aided Verification, New Brunswick:Lecture Notes in Computer Science,1996,1102:394-397.
[76]R. Milner. Communication and Concurrency. Prentice Hall,1989.
[77]Bowen Alpern, Fred B. Schneider. Defining liveness. Information Processing Letters,1985, 21:181-185.
[78]Rod Girle. Modal Logics and Philosophy. Acumen Press,2000.
[79]李磊.面向服务计算的若干关键技术研究：(博士学位论文),合肥：中国科学技术大学,2008.
[80]Yang Hongli, Zhao Xianpeng, Cai Chao, et al. Model-Checking of Web Services Choreography. Technical Report. In:Proc. of the 4th IEEE International Workshop on Service-Oriented Systems Engineering (SOSE 2008), Taiwan, IEEE CSP,2008.
[81]李景霞,候紫峰.Web服务组合综述.计算机应用研究,12：4-7.
[82]刘必欣.动态Web服务组合关键技术研究：(博士学位论文),长沙：国防科学技术大学,2005.
[83]M. Hennessy, R. Milner. Algebraic laws for nondeterminism and concurrency. J. Assoc. Comput. Mach.,1985,32:137-161.
[84]D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science,1983,27(3): 333-354.
[85]W.M.P. van der Aalst. Challenges in business process management:Verification of business processes using Petri nets. Bulletin of the EATCS,2003,80:174-191.
[86]Xiuguo Zhang, Weishi Zhang. A Cooperative Service Composition Language and Its Formal Semantics. In:Proc. of the 7th International Conference on Parallel and Distributed Computing, Applications and Technologies (PDCAT 2006), Taipei:IEEE Computer Society Press,2006.
[87]Xiuguo Zhang, Weishi Zhang. CCML:A Novel Service Composition Language, In:Proc. of WI-IAT'06 International Workshop on Service Composition, Hong Kong:IEEE Computer Society Press,2006.
[88]R. Keller. Formal verification of parallel programs. Comm. ACM,1976,19:371-384.
[89]刘方方,史玉良,张亮.基于进程代数的Web服务合成的替换分析.计算机学报,2007,30(11)：2033-2039.
[90]Roberto Chinnici, Jean-Jacques Moreau, Arthur Ryman, et al. Web Services Description Language (WSDL) Version 2.0. W3C Working Draft. Available at: http://www.w3.org/TR/2004/WD-wsdl20-20040803.
[91]David Martin, Mark Burstein, Jerry Hobbs, et al. OWL-S:Semantic Markup for Web Services. W3C Working Draft. Available at:http://www.w3.org/Submission/OWL-S/.
[92]高勇,刘瑜,谢昆青.一个基于Petri网的Web服务组合模型.计算机工程,2006,32(6)：17-19.
[93]唐达.基于层次细化Petri网的工作流参与者机制与动态特性研究.计算机研究与发展,2004,41(9)：1545-1552.
[94]廖名学,范植华.MPI程序同步通信基本模型死锁检测.电子学报,2008,36(2)：402-407.
[95]Pnueli A. A temporal logic of concurrent programs [A]. In:Proc. of the 18th IEEE Symposium on Foundation of Computer Science [C]. Providence:IEEE Computer Society Press,1977.
[96]Emerson E A, Clarke E M. Characterizing Correctness Properties of Parallel Programs Using Fixpoints [M]. Berlin:Springer Verlag,1980.
[97]Andrews T, Cubera F, Dholakia Y G H, et al. Business Process Execution Language for Web Services (BPEL4WS) 1.1. IBM Developworks. Available at:http://www-128.ibm.com/developerworks.
[98]Casati F, Sayal M, Shan M C. Developing e-services for composing e-services. In:Proc. of the 13th International'Conference on Advanced Information Systems Engineering (CAiSE2001), Interlaken, 2001:171-186
[99]Casati F, Ilnicki S, Jin L J, et al. Adaptive and Dynamic Service Composition in eFlow. In:Proc. of the International Conference on Advanced Information Systems Engineering, Stockholm,2000:13-31.
[100]Patil A, Oundhakar S, Sheth A, Verma K. METEOR-S Web service annotation framework[A], In: Proc. of the 13th International World Wide Web Conference (WWW2004)[C], New York,2004: 553-562.
[101]Shankar R P, Armando F. SWORD:A developer toolkit for Web service composition. In:Proc. of the 11th International World Wide Web Conference, Honolulu,2002:786-810.
[102]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.
[103]Richard Hull, Jianwen Su. Tools for composite web service:a short overview, ACM SIGMOD Record,2005,34(2):86-95.
[104]Benatallah B, Sheng Q Z, Dumas M. The Self-Serv Environment for Web Services Composition[J]. IEEE Internet Computing,2003,7(1):40-48.
[105]Schahram Dustdar, Wolfgang Schreiner. A survey on web services composition. Int. J. Web and Grid Services,2005,1(1):1-30.
[2]Mark Endrei, Jenny Ang, Ali Arsanjani, et al. Patterns:Service-Oriented Architecture and Web Services. IBM Technical Report. Available at: http://www.redbooks.ibm.com/redbooks/pdfs/sg246303.pdf.
[3]邓水光,李荧,吴健.Web服务行为兼容性的判定与计算.软件学报,2007,18(12)：3001-3014.
[4]Kramer L, Salaun G, Berardi D, Mecella M. When Are Two Web Services Compatible. In:Proc. of the 5th VLDB International Workshop on Technologies for e-Services (VLDB-TES),2004.
[5]Foster H, Uchitel S, Magee J, et al. Compatibility verification for web service choreography. In:Proc. of International Conference on Web Service (ICWS),2004.
[6]Wombacher A, Fankhauser P, Mahleko B, et al. Matchmaking for Business Processes based on Choreographies. International Journal of Web Services Research,2004,1(4):14-32.
[7]X. Fu, T. Bultan, J. Su. Analysis of Interacting BPEL Web Services. In:Proc. of 13th Int. Conf. World Wide Web (WWW), ACM Press,2004:621-630.
[8]Martens A. On compatibility of web services. Petri Net Newsletter.2003,65:12-20.
[9]H. Foster, S. Uchitel, J. Kramer, et al. Compatibility verification for web service choreography. In:Proc. of the 2th International Conference on Web Services,2004:738-741.
[10]H. Foster, S. Uchitel, J. Magee, et al. Model-based verification of web service compositions. In:Proc. of 18th IEEE International Conference on Automated Software Engineering,2003:152-163.
[11]H. Foster, S. Uchitel, J. Magee, et al. LTSA-WS:A Tool for Model-based Verification of Web Service Compositions and Choreography. In:Proc. of ICSE 2006:771-774.
[12]岳昆,于晓玲,周傲英.Web服务核心支撑技术：研究综述.软件学报,2004,15(3)：428-442.
[13]饶云,冯博琴,李尊朝.基于Web Services的服务合成技术综述.系统工程与电子技术,2005,27(8)：1481-1489
[14]G. J. Holzmann. The Spin Model Checher: Primer and Reference Manual. Boston:Addison-Wesley, 2004.
[15]冯名正.Web服务组合研究综述.计算机应用与软件,2007,24(2)：23-27.
[16]J. Misra, W. Cook. Computing Orchestration:A Basis for Wide-Area Computing. Journal of Software & Systems Modeling,2007,6(1):83-110.
[17]Nickolas Kavantzas, David Burdett, Gregory Ritzinge, et al. Web Services Choreography Description Language Version 1.0. W3C Working Draft.Available at: http://www.w3.org/TR/2004/WD-ws-cdl-10-20041217/.
[18]G. Diaz, J.J. Pardo, M.-E. et al. Automatic Translation of WS-CDL Choreographies to Timed Automata. In:Proc. of Int. Workshop on Web Services and Formal Methods (WS-FM2005), Springer, 2005:230-242.
[19]Tao X. F., Jiang C. J.. Formalizing Web service and modeling Web service based system based on object oriented Petri net. Lecture Notes in Computer Science. Berlin:Springer-Verlag,2004: 1008-1011.
[20]郭玉彬,杜玉越,系建清.Web服务组合的有色网模型及运算性质.计算机学报,2006,29(7)：1067-1075.
[21]X. Yi, K.J. Kochut. A CP-nets-based design and verification framework for web services composition. In:Proc. of the 2nd IEEE International Conference on Web Services,2004:756-760.
[22]K. Schmidt, C. Stahl. A Petri net semantic for BPEL4WS-validation and application. In:Proc. of the 11 the Workshop on Algorithms and Tools for Petri Nets,2004:1-6.
[23]Zhang Jia, Chung Jen Yao, Chang C. K., Kim S.. WS-Net:A petri-net based specification model for web service. In:Proc. of the 2nd IEEE International Conference on Web Services,2004:420-427.
[24]R.Hamadi, B.Benatallah. A Petri Net-based Model for Web Service Composition. In:Proc. of the 14th Australasian Database Conference on Database Technologies,2003: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 Wolfan. The Computer Journal,2001,44(4):246-279.
[28]M. Baldoni, C. Baroglio, A. Martelli, et al. Verifying the conformance of web services to global interaction protocols:a first step. In Proc of the 2nd International Workshop on Web Services and Formal Methods, Versailles:Lecture Notes in Computer Science,2005:257-271.
[29]肖美华,薛锦云.时态逻辑形式化描述并发系统性质.海军工程大学学报,2004,16(5)：10-13.
[30]辜希武.Web服务组合形式化模型研究：(博士学位论文),武汉：华中科技大学,2007.
[31]周永华,陆化普.基于Web服务的智能交通系统集成.计算机工程,2006,32(8)：244-246.
[32]J. E. Hopcroft, R. Motwani, J. D. Ullman. Introduction to Automata. Theory, Languages, and Computation (2nd Edition).Boston: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 Proc. of 12th International Conference on World Wide Web, Budapest: 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. Proc. of 8th International Conference on Implementation and Application of Automata,California:Lecture Notes in Computer Science,2003, 2759:188-200.
[35]G.Plotkin. Call-by-name, call-by-value, and the A,-Calculus. Theoretical Compute Science,1975,1: 125-159.
[36]付燕宁.Web服务组合方法研究：(博士学位论文),长春：吉林大学,2007.
[37]C.A.R.Hoare. Communicating Sequential Processes. New Jersey:Prentice-Hall,1985.
[38]Mads Dam. CCS:Processes and Equivalences. Technical Report. Available at: http://www.imit.kth.se/courses/2G1516/Docs05/Slides/CCS-lecture-1.5.pdf.
[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.Salaun, L.Bordeaux, M.Schaerf. Describing and Reasoning on Web Service using Process Algebra.In Proc. of the 2th IEEE International Conference on Web Services, California:IEEE Computer Society Press,2004:43-50.
[43]金仙力.实时服务构件的语义特征和行为组装形式化技术研究：(博士学位论文),北京：北京邮电大学,2008.
[44]A.Ferrara. Web services:a process algebra approach. In:M.Aiello, M.Aoyama, FCurbera, et al, eds. Proc. of 2th International Conference on Service Oriented Computing, New York, USA,2004. ACM Press,2004:242-251
[45]Rance Cleaveland, Tan Li, Steve Sims. The Concurrence Workbench of the New Century. User's Manual. Available at:http://www.cs.sunysb.edu/-cwb/.
[46]杨涛,刘锦德.Web Services技术综述—一种面向服务的分布式计算模式.计算机应用,24(8)：1-4.
[47]M. Butler, C. Ferreira, M.Y.Ng. Precise modeling of compensating business transactions and its applications to BPEL. Jounal of Universal Computer Science,2005,11(5):712-743.
[48]Van der Aalst WMP. The Application of Workflow Management[J]. Journal of Circuits, Systems and Computers,1998,8(1):21-66.
[49]B. F Chellas. Modal Logic:An Introduction. Cambridge University Press,1980.
[50]M. H. ter Beek, A. Bucchiarone, S. Gnesi. Formal Methods for Serivce Composition. Technical Report. Software/Program Verification, Formal Methods, ACM.
[51]M. H. ter Beek, A. Bucchiarone, S. Gnesi. A Survey on Serivce Composition Approaches:From Industrial Standards to Forml Methods. Technical Report. Software/Program Verification, Formal Methods, ACM.
[52]阎志华,丁秋林.基于Petri网的Web服务流程建模.计算机应用,23(12)：55-57.
[53]Bucchiarone, Gnesi. A Survey on Serivce Composition Language and Models. In:Proc. of International Workshop on Web Service Modeling and Testing,2006:51-63.
[54]E. A. Emerson, C. L. Lei. Efficient model checking in fragments of the propositional mu-calculus. In: Proc. of the Symposium on Logic in Computer Science (LISC'86), Cambrige:IEEE Computer Society Press,1986:267-278
[55]Jensen K.. Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Volume 1, Basic Concepts, Monographs in Theoretical Computer Science. Springer-Verlag,1997.
[56]Luca Aceto, Kim G. Larsen. An Introduction to Milner's CCS. Technical Report, Department of Computer Science, Aalborg University, Aalborg, Denmark, March 2005. Available at: http://www.dimi.uniud.it/miculan/Didattica/MFGC04/intro2ccs.pdf.
[57]Leslie Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering,1977,3(2):125-143.
[58]葛声,马殿富,胡春明.基于Web服务的网络软件运行平台研究与实现.北京航空航天大学学报,2003,29(10)：897-900.
[59]Beard B, Bidoit M, Finkel. System and Software Verification:Model Checking Techniques and Tools. Berlin:Springer-Verlag,2001.
[60]Wil van der Aalst, Kees van Hee工作流管理-模型、方法和系统.北京：清华大学出版社,2004.
[61]Emerson E A, Haopen J Y. "Sometimes" and "Not Never" revised:on branching versus Linear time temporal logic [J]. Journal of the ACM,1986,9(1):12-17.
[62]廖军.面向服务计算(SOC)中服务组合的研究：(博士学位论文),武汉：华中科技大学,2007.
[63]倪晚成,刘连臣,吴澄.Web服务组合方法综述.计算机工程,2008,32(4)：79-81.
[64]蒋哲远,韩江洪,王钊.动态的QoS感知Web服务选择和组合优化模型.计算机学报,2006,32(5)：1015-1025.
[65]黄小庆,夏安邦.基于有色Petri网和分类服务的Web服务组合模型.计算机集成制造系统.2009,15(1)：53-62.
[66]周相兵,杨小平,向昌成,谢成锦.面向本体的语义服务组合评价模型研究.计算机集成制造系统,2008,14(12)：2346-2353.
[67]陈彦萍,李增智,唐亚哲.一种满足马尔可夫性质的不完全信息下的Web服务组合方法.计算机学报,2006,29(7)：1167-1178.
[68]陈彦萍,李增智,郭志胜.Web服务组合中基于服务质量的服务选择算法.西安交通大学学报,2006,40(8)：897-905.
[69]李喜彤,范玉顺.Web服务过程建模及其逻辑正确性验证.计算机集成制造系统,2008,14(4)：675-682.
[70]廖军,谭浩,刘锦德.基于Pi-演算的Web服务组合的描述和验证.计算机学报,2005,28(4)：635-643.
[71]Biplav Srivastava, Jana Koehler. Web Service Composition:Current Solutions and Open Problems. In: In:Proc. of the 13th International Conference on Automated Planning & Scheduling (ICAPS 2003), Workshop on Planning for Web Services,2003:28-35.
[72]高勇,刘瑜.一个基于Petri网的Web服务组合模型.计算机工程,32(6),2006：17-19.
[73]张秀国.基于过程网络的服务协同计算模型研究：(博士学位论文),大连：大连海事大学,2006.
[74]Li Bao, Weishi Zhang, Xiuguo Zhang. Describing and Verifying Web Service Using CCS. In:Proc. of the 7th International Conference on Parallel and Distributed Computing, Applications and Technologies,2006.
[75]R. Cleaveland and S. Sims. The NCSU concurrency workbench. In R. Alur and T. Henzinger, editors, Proc. of the 8th International Conference on Computer Aided Verification, New Brunswick:Lecture Notes in Computer Science,1996,1102:394-397.
[76]R. Milner. Communication and Concurrency. Prentice Hall,1989.
[77]Bowen Alpern, Fred B. Schneider. Defining liveness. Information Processing Letters,1985, 21:181-185.
[78]Rod Girle. Modal Logics and Philosophy. Acumen Press,2000.
[79]李磊.面向服务计算的若干关键技术研究：(博士学位论文),合肥：中国科学技术大学,2008.
[80]Yang Hongli, Zhao Xianpeng, Cai Chao, et al. Model-Checking of Web Services Choreography. Technical Report. In:Proc. of the 4th IEEE International Workshop on Service-Oriented Systems Engineering (SOSE 2008), Taiwan, IEEE CSP,2008.
[81]李景霞,候紫峰.Web服务组合综述.计算机应用研究,12：4-7.
[82]刘必欣.动态Web服务组合关键技术研究：(博士学位论文),长沙：国防科学技术大学,2005.
[83]M. Hennessy, R. Milner. Algebraic laws for nondeterminism and concurrency. J. Assoc. Comput. Mach.,1985,32:137-161.
[84]D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science,1983,27(3): 333-354.
[85]W.M.P. van der Aalst. Challenges in business process management:Verification of business processes using Petri nets. Bulletin of the EATCS,2003,80:174-191.
[86]Xiuguo Zhang, Weishi Zhang. A Cooperative Service Composition Language and Its Formal Semantics. In:Proc. of the 7th International Conference on Parallel and Distributed Computing, Applications and Technologies (PDCAT 2006), Taipei:IEEE Computer Society Press,2006.
[87]Xiuguo Zhang, Weishi Zhang. CCML:A Novel Service Composition Language, In:Proc. of WI-IAT'06 International Workshop on Service Composition, Hong Kong:IEEE Computer Society Press,2006.
[88]R. Keller. Formal verification of parallel programs. Comm. ACM,1976,19:371-384.
[89]刘方方,史玉良,张亮.基于进程代数的Web服务合成的替换分析.计算机学报,2007,30(11)：2033-2039.
[90]Roberto Chinnici, Jean-Jacques Moreau, Arthur Ryman, et al. Web Services Description Language (WSDL) Version 2.0. W3C Working Draft. Available at: http://www.w3.org/TR/2004/WD-wsdl20-20040803.
[91]David Martin, Mark Burstein, Jerry Hobbs, et al. OWL-S:Semantic Markup for Web Services. W3C Working Draft. Available at:http://www.w3.org/Submission/OWL-S/.
[92]高勇,刘瑜,谢昆青.一个基于Petri网的Web服务组合模型.计算机工程,2006,32(6)：17-19.
[93]唐达.基于层次细化Petri网的工作流参与者机制与动态特性研究.计算机研究与发展,2004,41(9)：1545-1552.
[94]廖名学,范植华.MPI程序同步通信基本模型死锁检测.电子学报,2008,36(2)：402-407.
[95]Pnueli A. A temporal logic of concurrent programs [A]. In:Proc. of the 18th IEEE Symposium on Foundation of Computer Science [C]. Providence:IEEE Computer Society Press,1977.
[96]Emerson E A, Clarke E M. Characterizing Correctness Properties of Parallel Programs Using Fixpoints [M]. Berlin:Springer Verlag,1980.
[97]Andrews T, Cubera F, Dholakia Y G H, et al. Business Process Execution Language for Web Services (BPEL4WS) 1.1. IBM Developworks. Available at:http://www-128.ibm.com/developerworks.
[98]Casati F, Sayal M, Shan M C. Developing e-services for composing e-services. In:Proc. of the 13th International'Conference on Advanced Information Systems Engineering (CAiSE2001), Interlaken, 2001:171-186
[99]Casati F, Ilnicki S, Jin L J, et al. Adaptive and Dynamic Service Composition in eFlow. In:Proc. of the International Conference on Advanced Information Systems Engineering, Stockholm,2000:13-31.
[100]Patil A, Oundhakar S, Sheth A, Verma K. METEOR-S Web service annotation framework[A], In: Proc. of the 13th International World Wide Web Conference (WWW2004)[C], New York,2004: 553-562.
[101]Shankar R P, Armando F. SWORD:A developer toolkit for Web service composition. In:Proc. of the 11th International World Wide Web Conference, Honolulu,2002:786-810.
[102]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.
[103]Richard Hull, Jianwen Su. Tools for composite web service:a short overview, ACM SIGMOD Record,2005,34(2):86-95.
[104]Benatallah B, Sheng Q Z, Dumas M. The Self-Serv Environment for Web Services Composition[J]. IEEE Internet Computing,2003,7(1):40-48.
[105]Schahram Dustdar, Wolfgang Schreiner. A survey on web services composition. Int. J. Web and Grid Services,2005,1(1):1-30.