摘要
Web服务组合使得开发者可以基于面向服务的计算无缝地访问众多分布式服务，组合在一起解决复杂问题。大多数Web服务是独立开发并运行在异构平台上的，为了能够实现它们之间的服务组合，需要能够兼容其异构性的服务组合描述方法以及对组合后的服务进行验证或测试的方法。
本文在总结以前的研究结果的基础上，以Pi-演算为基础，建立了Web服务形式化描述模型PiFM4WS，对Web服务以及Web服务组合的主要行为进行描述，为Web服务组合的动态体系结构提供统一的描述方法；将基于不同视角的Web服务组合描述规范的主要行为映射到PiFM4WS中，说明经过映射之后的两类描述规范具有等价性；将类型系统加入PiFM4WS模型中，细化了Web服务的相容性，提出可替换性的概念和验证方法；在PiFM4WS模型中对服务网络进行描述，为实现Web服务组合的自动化提供理论基础。本文所取得的主要研究成果如下：
(1)建立Web服务形式化描述模型PiFM4WS：给出Web服务外部和内部行为的描述，即PiFM4WS的语法结构定义；给出Web服务经由交互发生组合的行为，即PiFM4WS的同构规则和操作语义。
(2)为两类基于不同视角的描述规范的主要行为提供映射规则：为BPEL4WS规范以及WS-CDL规范的概念和各类行为提供PiFM4WS的描述方法，从语法定义和操作语义的角度说明两类不同规范的等价性，并指出PiFM4WS提供的对动态体系结构的描述方法是现有描述规范无法实现的。
(3)基于类型化PiFM4WS的Web服务组合验证：将类型系统加入PiFM4WS中，根据子类型的关系细化Web服务的相容性，给出Web服务的可替换性的定义；根据信道是否和业务流程相关进行分类，结合Pi-演算中的代换算法，提出在动态体系结构下的Web服务可替换性的验证方法。
(4)对服务网络进行形式化描述，为实现Web服务自动组合提供理论基础：将抽象服务和具体服务之间的通信信道进行结构的抽象和描述，为服务关系的形式化描述建立理论基础。
综上所述，本文提出的形式化描述模型PiFM4WS、类型化的PiFM4WS以及服务网络的形式化描述，为Web服务组合提供了统一的形式化描述和验证框架，为实现Web服务的自动组合和验证提供了理论基础。
Web service composition allows developers to compose numerousservices to solve complex problem based on service-oriented distributedcomputing. Most Web services are developed independently and runningon heterogeneous platforms, in order to achieve the combination ofservices between them, service composition description method andverification(testing) method are need to compatible with heterogeneous.This paper summarizes the results of previous study, establish the formaldescription model PiFM4WS of Web services based on Pi-calculus. TheWeb service and the main acts of Web service composition are describedin the model mentioned above, and a unified description method isproposed for dynamic Web service composition architecture. Differentperspectives based Web service composition description specificationsare mapped to PiFM4WS main acts, and the equivalence betweendifferent descriptions after mapping is proofed. The PiFM4WS model hastype system to refine Web services compatibility, and support the conceptof replaceability and verification methods. The PiFM4WS model is usedto describe the service network, and provide theoretical basis of the Webservice automation composition. The main research results obtained areas follows:
(1) Establish formal description model PiFM4WS of Web services. ThePiFM4WS syntax structure definition provides description of external andinternal behavior of Web services. The PiFM4WS isomorphic rules andoperational semantics provide the interactions behaviors occur throughWeb service combination.
(2) Provides mapping rules for the description of main behavioral of twodifferent perspectives: The description methods of PiFM4WS areprovided for the concepts and acts of BPEL4WS specification andWS-CDL specification. The equivalence of different specifications isproofed from the perspective of syntax and operational semantics. Thedynamic architecture description method provided in PiFM4WS, can notbe achieved in other existing models.
(3) Provides Web services composition validation based on typed model PiFM4WS. The type system is added to PiFM4WS, and base on it,replaceability definition is proposed according to the relationship betweensubtypes and refines Web service compatibility. Replaceabilityverification method under the dynamic architecture of Web services isproposed according to the channel classification of process-related andcombining Pi-calculus substitution algorithm.
(4) Formal description of the service network provides a theoretical basisof automatic Web service composition. The communication channelstructure between abstract services and concrete services is abstracted anddescribed, which establish theoretical foundation of the formaldescription of service relationship.
In summary, this paper presents the formal description model PiFM4WS,the typed PiFM4WS and formal description of service network provide aunified formal description and verification framework, and providetheoretical basis for Web services automatic composition.
引文
[1]杨芙清．软件工程技术发展思索[J]．软件学报，2005,16(1):1~7．
[2] Tim Bray, Jean Paoli, C.M. Sperberg-McQueen, Eve Maler, et al. ExtensibleMarkup Language (XML)1.1(Second Edition)
[EB/OL]．http://www.w3.org/TR/2006/REC-xml11-20060816/.2006．
[3] E.Christensen, F.Curbera, G.Meredith, S.Weerawarana. Web Services DescriptionLanguage(WSDL)1.1[EB/OL].http://www.w3.org/TR/2001/NOTE-wsdl-20010315/.2001．
[4] Martin Gudgin, Marc Hadley, Jean-Jacques Moreau, et al. Soap version1.2W3CWorking Draft[EB/OL].http://www.w3.org/TR/2001/WD-soap12-part0-20011217/.2011．
[5] F. Curbera et al. The Next Step in Web Services[C]. Communications of the ACM.2003,46(10):29–34.
[6] M.P Papazoglou. Introduction: Service-oriented computing [C]. Communicationsof the ACM.2003,46(10):24-28.
[7] M.N. Huhns, M.P. Singh. Service-Oriented Computing: Key Concepts andPrinciples[C]. Internet Computing, IEEE.2005,9(1):75-81.
[8]岳昆，王晓玲，周傲英．Web服务核心支撑技术:研究综述[J]．软件学报，2004，15(3):428-442．
[9] IBM Services Architecture Team．Web Services architectureoverview[EB/OL]．http://www.ibm.com/developerworks/webservices/library/w-ovr/.2007．
[10] World Wide Web Consortium．Web ServicesArchitecture[EB/OL]．http://www.w3.org/TR/ws-arch/.2007．
[11] YANG J．Web service componentization[C]. Communications of the ACM．2003,46(10):35~40.
[12] L De Alfaro，Henzinger TA．Interface automata[C]. Proc．of the9th Annual ACMSyrup on the Foundations of Software Engineering(FSE2001)．2001:109~120．
[13] L de Alfaro，Henzinger TA，Stoelinga M．Timed interfaces[C]. SangiovanniVincentelli A,Sifakis J(eds) on Embedded Software(EMSOFT2002), LNCS2491.2002:108~122．
[14] Beyer D, Chakrabarti A，Henzinger TA．Web service interfaces[C]. InternationalWorld Wide Web Conference, Proceedings of the14th international conference WorldWide Web, Chiba, Japan.2005:148~159．
[15]陈振邦，王戟，董威，齐治昌．面向服务软件体系结构的接口模型[J]．软件学报，2006,17(6):1459~1469．
[16] A. Bucchiarone, S.Gnesi. A Survey on Services Composition Languages andModels[C]. In Proceedings of the International Workshop on Web Services Modelingand Testing, Palermo, Italy.2006:51-63.
[17] R. Dijkman, M. Dumas. Service-oriented Design: A Multi-viewpointApproach[J]. International Journal of Cooperative Information Systems,2004,13(4):337-368
[18] T. Andrews, F. Cubera, H. Dholakia, et al. Business Process Execution Languagefor Web Services Versionl.l[EB/OL].http://www-128.ibm.com/developerworks/library/specification/ws-bpel/.2007.
[19] N. Kavantzas, D. Burdett, G Rizinger, et al. Web Service ChoreographyDescription Language Version1.0[EB/OL]. http://www.w3.org/TR/ws-cdl-10/.2007.
[20] A. Arkin, S. Askary, S. Fordin, et al. Web Service Choreography Interface (WSCI)1.0[EB/OL]. http://www.w3.org/TR/wsci/.2007.
[21] R. Hull, J.Su.Tools for Composite Web Services: A Short Overview[C].Newsletter ACM SIGMOD Record.2005,34(2):86-95.
[22] R.Hamadi, B.Benatallah. A Petri Net-based Model for Web ServiceComposition[C]. Proceeding ADC '03Proceedings of the14th Australasian databaseconference, Adelaide, Australia.2003(17):191-200
[23] WM.P van der Aalst, A.H.M. ter Hofstede. Verification of Workflow TaskStructures: A Petri-Net-Based Approach[J]. Information Systems,2000,25(1):43-69.
[24] Y. Yang, Q. Tan, and Y. Xiao. Verifying web services composition based onhierarchical colored Petri nets[C]. Proceeding IHIS '05Proceedings of the firstinternational workshop on Interoperability of heterogeneous information systems,Bremen, Germany.2005:47-54.
[25] Yang, Q.Tan, Y.Xiao, J.Yu, and F.Liu. Exploiting hierarchical CP-nets to increasethe reliability of web services workflow[C]. Proceeding of the InternationalSymposium on Applications and the Internet, Phoeniz, AZ, USA.2006:116-122.
[26]张文涛，彭泳，陈俊亮．基于Petri网的Web服务自动组合研究[J]．计算机学报，2006,29(7):1058-1066．
[27] D.Berardi, D.Calvanese, G De Giacomo, et al. Automatic Services Compositionbased on Behavior Descriptions[J]. International Journal of Cooperative InformationSystems.2005,14(4):333-376.
[28] D.Berardi, G De Giacomo, M. Lenzerini, et al. Synthesis of underspecifiedcomposite e-services based on automated reasoning[C]. Proceedings of2thInternational Conference on Service-Oriented Computing, New York, USA,2004.ACM Press,2004:105-114.
[29] T.Bultan, X.Fu, R.Hull, J. Su. Conversation Specfication: A new approach todesign and analysis of e-service composition[C]. Proceedings of12th InternationalConference on World Wide Web, Budapest, Hungary,2003. ACM Press,2003:403-410.
[30]张文涛，彭泳，陈俊亮．会话类E-Service的接口兼容和服务组合分析[J]．计算机学报，2006,29(7):1047-1056．
[31] J.C.M Baeten. A brief history of process algebra[J]. Theoretical ComputerScience,2005,335(2-3):131-146
[32] G.Plotkin. Call-by-name, call-by-value, and the-Calculus[J]. TheoreticalComputer Science,1975,1:125-159
[33] C.A.R. Hoare. Communicating Sequential Processes[J]. MagazineCommunications of the ACM,1978,21(8):666-677.
[34] R. Milner. A Calculus of Communicating Systems. Lecture Notes in ComputerScience,1980, Volume92
[35] R. Milner, J.Parrow, D.Walker. A calculus of mobile process (Parts I and II)[J].Information and Computation,1992,100(1):1-77.
[36] T. Bolognesi, E. Brinksma. Introduction to the ISO Specification LanguageLOTOS[J]. Computer Network and ISDN Systems,1987,14(1):25-59.
[37] E. Oren, A. Haller. Formal Frameworks for Workflow Modelling [DERITechnical Report2005-4-07]. Galway, Ireland: Digital Enterprise Research Institude,National University of Ireland,2005.
[38] L. Bordeaux and G. Salaun. Using process algebra for web services: Earlyresultsand perspectives[J]. Lecture Notes in Computer Science,2004,3324:54-68.
[39] G.Salaiin, L.Bordeaux, M.Schaerf. Describing and Reasoning on Web Servicesusing Process Algebra[C]. Proceedings of the2th IEEE International Conference onWeb Services, California, USA,2004. Washington DC,USA:IEEE Computer SocietyPress,2004:43-50.
[40] A. Brogi, C. Canny E. Pimentel. Formalizing Web Service Choreographies[J].Electronic Notes in Theoretical Computer Science,2004,105:73-94.
[41] J. Camara, C. Canal, J.Cubo. Issues in the formalization of Web ServiceOrchestrations[C]. Proceedings of2th International Workshop on Coordination andApplication Techniques for Software Entities, Glasgow, Scotland,2005:17-24.
[42] F. Puhlmann, M. Weske. Using the Pi-Calculus for Formalizing WorkflowPatterns[C]. Proceedings of3th International Conference on Business ProcessManagement, Nancy, France,2005:153-168.
[43] F. Puhlmann. Why do we actually need the Pi-Calculus for Business ProcessManagement[C]. Proceedings of9th International Conference on BusinessInformation Systems (BIS2006), Klagenfurt, Austria,2006,85:77-89.
[44] S.J. Woodman, D.J. Palmer, S.K. Shrivastava, et al. Notations for theSpecification and Verification of Composite Web Services[C]. Proceedings of the8thIEEE International Enterprise Distributed Object Computing Conference., California,USA,2004. Washington DC,USA:IEEE Computer Society Press,2004:35-46.
[45]廖军，谭浩，刘锦德．基于Pi-演算的Web服务组合的描述和验证[J]．计算机学报，2005,28(4):635-643．
[46] A.Ferrara. Web services: a process algebra approach[C]. Proceedings of2thInternational Conference on Service Oriented Computing, New York, USA,2004.ACM Press,2004:242-251.
[47] G. Salaiin, A. Ferrara, and A. Chirichiello. Negotiation among web services usingLOTOS/CADP[J]. Lecture Notes in Computer Science,2004,3250:198-212.
[48] H. Foster, S. Uchitel, J. Kramer, et al. Compatibility verification for web servicechoreography[C]. Proceedings of the2th International Conference on Web Services,California, USA,2004. Washington DC, USA:IEEE Computer Society Press,2004:738-741.
[49] H. Foster, S. Uchitel, J. Magee, et al. Using a rigorous approach for engineeringweb service compositions: a case study[C]. Proceedings of the2005IEEEInternational Conference on Services Computing, Orlando, USA,2005. WashingtonDC, USA:IEEE Computer Society Press,2005,1:217-224.
[50] M. Koshkina, F. van Breugel. Modelling and verifying web service orchestrationby means of the concurrency workbench[C]. ACM SIGSOFT Software EngineeringNotes,2004,29(5):1-10.
[51] M. Koshkina. Verification of business processes for web services [Master'sthesis]. Toronto, Canada:York University,2003.
[52] M. Viroli. Towards a formal foundation to orchestration languages[C].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.
[53] H. Foster, S. Uchitel, J. Magee,et al. Model-Based analysis of Obligations in WebService Choreography[C]. Proceedings of the Advanced International Conference onTelecommunications and International Conference on Internet and Web Applicationsand Services, Guadeloupe, French,2006. Washington DC, USA: IEEE ComputerSociety Press,2006:149-157.
[54]杨鑫，陈俊亮．WSC/ADL: Web服务组合系统体系结构描述语言[J]．软件学报，2006,17(5):1182-1194．
[55]陈彦萍，李增智，唐业哲等．一种满足马尔可夫性质的不完全信息下的Web服务组合方法[J]．计算机学报，2006,29(7):1167-1178．
[56]辜希武，卢正鼎．基于Pi-演算的BPEL4WS Web服务组合形式化模型[J]．计算机科学，2007,34(3):69-74．
[57]辜希武，卢正鼎．Web服务编排描述语言WS-CDL的形式化模型框架[J]．计算机科学，2007,34(9):5-11．
[58]辜希武，卢正鼎．类型化的Web服务组合形式化模型[J]．计算机科学，2008,35(1):128-134．
[59] Solanki M. Cau A. Zedan H. Augmenting Semantic Web Service Descriptionwith Compositional Specification[C]. Proceeding of World Wide Web2004，NewYork, NY, USA: ACM Press,2004:544-552．
[60]雷丽晖，段振华．一种基于扩展有限自动机验证组合Web服务的方法[J]．软件学报．2007,12(18):2980-2990．
[61] Xiang Fu，Tevfik Bultan，Jianwen Su．Analysis of interacting BPEL webservices[C]. Proceedings of thel3th International Conference on World Wide Web2004. New York, ACM Press,2004:621-630.
[62] Xiang Fu,Tevfik Bultan，Jianwen Su．WSAT：A Tool for Formal Analysis of WebServices[C]. Proceedings of the16th International Conferece on Computer AidedVerification．Lecture Notes in Computer Science,2004,3114:510-514.
[63] Xiang Fu，Tevfik Bultan，Jianwen Su．Synchronizability of Conversations amongWeb Services[C]. IEEE Transactions on Software Engineering,2005,31(12):1042-1055．
[64] Andreas Wombacher, Peter Fankhauser, Bendick Mahleko．Matchmaking forBusiness Processes based on Choreographies[C]. Proceedings of the IEEEInternational Conference on e-Technology, e-Commerce and e-Service,2004,3:359-368．
[65] M. Dam. Model Checking Mobile Processes[J]. Lecture Notes in ComputerScience,1993,715:22-36.
[66] B.Victor, F.Moller. The Mobility Workbench-A Tool for the Pi-Calculus[C].Proceedings of the6th International Conference on Computer Aided Verification,California, USA,1994. Springer, Lecture Notes in Computer Science,1994,818:428-440.
[67]辜希武，卢正鼎．Web服务编相容性的形式描述与分析[J]．计算机工程与应用，2007,43(27):28-33．
[68] C.Canal, L.Fuentes, E.Pimentel, et al. Adding Roles to CORBA Objects[C].IEEE Transactions on Software Engineering.2003,29:242-260.
[69] Yuliang Shi, Liang Zhang, Fangfang Liu, et al. Compatibility Analysis of WebServices[C]. Proceedings of the2005IEEE/WIC/ACM International Conference onWeb Intelligence, Compiegne, France,2005. Washington DC,USA:IEEE ComputerSociety Press,2005:483-486.
[70] YunYao Li, H.V Jagadish. Compatibility Determiation in Web Services[C].Proceedings of the first International E-Services Workshop, Pittsburgh, USA,2003:7-15.
[71]M.Mecella, B.Pernici, P.Craca. Compatibility of e-Services in a CooperativeMulti-platform Environment[J]. Lecture Notes in Computer Science,2001,2193:44-57.
[72] V.De Antonellis, M.Melchiori, B.Pernici, et al. A Methodology for e-ServiceSubstitutability in a Virtual District Environment[C]. Proceedings of the15thInternational Conference on Advanced Information Systems Engineering, Klagenfurt,Austria,2003. Springer, Lecture Notes in Computer Science,2003,2681:552-567.
[73] V.De Antonellis, M.Melchiori, P.Plebani. An approach to Web servicecompatibility in cooperative processes[C]. In Proceedings of the2003Symposium onApplications and the Internet Workshops,2003, Washington DC, USA: IEEEComputer Society Press,2003:95-100.
[74] L.Bordeaux, GSalaiin, D.Berardi, et al. When are two Web Services Compatible
[C]. Proceedings of the5th International Workshop on Technologies for E-Services,Toronto, Canada,2004. Springer, Lecture Notes in Computer Science,2004,3324:15-28.
[75] Fangfang Liu, Liang Zhang, Yuliang Shi, et al. Formal analysis of Compotibilityof Web Services via CCS[C]. Proceedings of the International Conference on NextGeneration Web Services Practices, Seoul, Korea,2005. Washington DC, USA: IEEEComputer Society Press,2005:143-148.
[76] J.Mendling, M.Hafner. From WS-CDL Choreography to BPEL ProcessOrchestration[EB/OL].http://wi.wu-wien.ac.at/home/mendling/publications/TR06-CDL.pdf.2007.
[77] P. Wohed, WM.P van de Aalst, M. Dumas, et al. Pattern Based Analysis ofBPEL4WS [FIT-TR-2002-04Technical Report]. Queensland, Australia:QueenslandUniversity of Technology,2003
[78] J.Li, J.He, G.Pu, and H.Zhu. Towards the semantics for web servicechoreography description language[J]. Lecture Notes in Computer Science.Springer,2006,4260:246-263.
[79] B.C Pierce. Types and Programming Languages[M]. Massachusetts, USA: TheMIT Press,2002.
[80] R.Milner. The Polyadic Pi-Calculus: a Tutorial [Technical ReportECS-LFCS-91-180]. Edinburgh, UK: Laboratory of Foundations of ComputerScienec, Computer Science Department, University of Edinburg,1991.
[81] B.Pierce, D. Sangiorgi. Typing and Subtyping for Mobile Processes[J]. Journal ofMathematical Structures in Computer Science,1996,6(5):409-453.
[82] Sangiorgi D, Walker D.The Pi-calculus: a Theory of Mobile Processes[M].Cambridge: Cambridge University Press,2001
[83] Jun Sun, Yang Liu, et al. Model-based Methods for Linking Web ServiceChoreography and Orchestration[C]. The17th Asia Pacific Software EngineeringConference).Sydney, Australia,2010:166-175.
[84] J.S.Dong, Y Liu, et al. Verification of Computation Orchestration Via TimedAutomata[C]. ICFEM'06Proceedings of the8th international conference on FormalMethods and Software Engineering, Springer-Verlag Berlin, Heidelberg,2006:226-245.
[85] G. Pu, J. Shi, et al. The Validation and Verification of WSCDL[C]. APSEC '07Proceedings of the14th Asia-Pacific Software Engineering Conference, IEEEComputer Society Washington DC, USA,2007:81-88.
[86] R.Kazhamiakin, P.Pandya, Marco Pistore. Representation, Verification, andComputation of Timed Properties in Web[C]. ICWS'06Proceedings of the IEEEInternational Conference on Web Services, IEEE Computer Society Washington DC,USA,2006:497-504.
[87] R. Kazhamiakin, M. Pistore. Choreography conformance analysis:Asynchronous communications and information alignment[C]. WS-FM'06Proceedings of the Third international conference on Web Services and FormalMethods, Springer-Verlag Berlin, Heidelberg,2006:227-241.
[88] M. Baldoni, C. Baroglio, et al. Verifying the conformance of web services toglobal interaction protocols: A first step[C]. EPEW'05/WS-FM'05Proceedings of the2005international conference on European Performance Engineering, and WebServices and Formal Methods, international conference on Formal Techniques forComputer Systems and Business Processes, Springer-Verlag Berlin, Heidelberg,2005:257-271.
[89] WM.P.vd.Aalst, M.Dramas, C.Onyang, et al. Conformance checking of servicebehavior[J]. ACM Transactions on Internet Technology (TOIT),2008,8(3):1-30.
[90] H. Foster, W.Emmerich, J.Kramer, et al. Model Checking Service Compositionsunder Resource Constraints[C]. ESEC-FSE '07Proceedings of the6th joint meetingof the European software engineering conference and the ACM SIGSOFT symposiumon The foundations of software engineering, ACM New York, USA,2007:225-234.
[91] H. Foster, S. Uchitel, J. Magee, et al. LTSA-WS: a Tool for Model-BasedVerification of Web Service Compositions and Choreography[C]. ICSE '06Proceedings of the28th international conference on Software engineering, ACM NewYork, USA,2006:771-774.
[92]辜希武，卢正鼎．类型化的Web服务组合形式化模型[J]．计算机科学．2008,35(1):128-134．
[93] D. SANGIORGI. A Theory of Bisimulation for the pi-Calculus[J]. ActaInformatica,1996,3(1):69-97.
[94] Yuxi Fu. Bisimulation congruence of Pi-calculus[J]. Information andComputation,2003,184(1):201-226
[95] HEP M, LEYMANN F, DOMINGUE F, et al. Semantic business processmanagement: a vision towards using semantic Web services for business processmanagement[C]. Proc of IEEE International Conference on e-BusinessEngineering．Washington DC: IEEE Computer Society.2005:535~540.
[96] PISTORE M, TRAVERSO P, BERTOLI P, et al. Automated synthesis ofcomposite BPEL4WS Web service[C]. Proc of IEEE International Conference on Webservice, Washington DC: IEEE Computer Society.2005:293~301.
[97]陈世展，冯志勇．服务网络：Web服务组合的新基点[J]．计算机应用研究，2008,25(5):1378~1382．