Web服务组合的性质检验与实现
|
摘要
随着Web服务的出现和推广,基于Web服务的动态组合技术已成为近年来的研究热点。Web服务的业务流程执行语言(BPEL4WS)作为一种基于业务流程的服务组合方法,建模理论基础比较薄弱,组合正确性比较难以保证,所以Web服务组合的验证就显得十分重要,在服务被正式实施之前,必须通过验证来考查流程的正确性,无死锁性等问题。
在这样的前提下,本文提出利用Pi演算和mu演算对BPEL4WS进行性质检验的方法,并开发出一个性质检验工具,对Web服务组合进行检验,包括安全性检验和可达性检验。
该工具基本上实现了BPEL4WS的自动化检验,对检验时发现不满足性质的,则对错误处的片段进行标注,并把错误路径反馈到BPEL4WS源文件中。
对用户来说,检验过程基本是一个透明的过程,用户不用深入了解具体的检验方法和知识,就可以直接利用本文开发的工具进行性质检验,并可针对检验后标识的地方进行改进。本文的结果说明对BPEL4WS文件的自动化性质检验和出错路径标识是可行的。
Along with the prosperity and acceptance of the Web services, the technique of dynamic service composition based on Web Services has been regarded as one of the hot research topics. The Business Process Execution Language for Web services (BPEL4WS), as a service composition method based on business process, is weak in modeling and compositing. So the validity of the process and the property of non-deadlocks must be simulated and proved before the service composition is being implemented formally.
According to the requirement mentioned above, using Pi-calculus and mu-calculus, a method for checking the property of BPEL4WS has been put forward in this thesis, as well as a tool for checking reachable and deadlocks.
People could check BPEL4WS files roughly automatic on, when it finds error, it will tag error on BPEL4WS files.
It is almost transparent, from modeling to checking, to user, the user who doesn’t understand the formal method thoroughly, can do the check using the tool and do the improvement at the tagged place. The simulation result shows that it is feasible to check the property of BPEL4WS and tag the error path automatically.
在这样的前提下,本文提出利用Pi演算和mu演算对BPEL4WS进行性质检验的方法,并开发出一个性质检验工具,对Web服务组合进行检验,包括安全性检验和可达性检验。
该工具基本上实现了BPEL4WS的自动化检验,对检验时发现不满足性质的,则对错误处的片段进行标注,并把错误路径反馈到BPEL4WS源文件中。
对用户来说,检验过程基本是一个透明的过程,用户不用深入了解具体的检验方法和知识,就可以直接利用本文开发的工具进行性质检验,并可针对检验后标识的地方进行改进。本文的结果说明对BPEL4WS文件的自动化性质检验和出错路径标识是可行的。
Along with the prosperity and acceptance of the Web services, the technique of dynamic service composition based on Web Services has been regarded as one of the hot research topics. The Business Process Execution Language for Web services (BPEL4WS), as a service composition method based on business process, is weak in modeling and compositing. So the validity of the process and the property of non-deadlocks must be simulated and proved before the service composition is being implemented formally.
According to the requirement mentioned above, using Pi-calculus and mu-calculus, a method for checking the property of BPEL4WS has been put forward in this thesis, as well as a tool for checking reachable and deadlocks.
People could check BPEL4WS files roughly automatic on, when it finds error, it will tag error on BPEL4WS files.
It is almost transparent, from modeling to checking, to user, the user who doesn’t understand the formal method thoroughly, can do the check using the tool and do the improvement at the tagged place. The simulation result shows that it is feasible to check the property of BPEL4WS and tag the error path automatically.
引文
[1]www.w3.org/TR/soap,2001
[2]Web Services Description Language 1.2 www.w3.org/TR/wsdl
[3]http://uddi.org/pubs/uddi-v3.00-published-20020719.htm.
[4]Matskin, Mihhail, and Rao, Jinghai. Value-Added Web Services Composition Using Automatic Program Synthesis. Springer-Verlag Berlin Heidelberg, LNCS 2512, 2002, pp.213-224.
[5]IBM. IBM Web Services Tutorial. http://www-106.ibm.eom/develoPerworks/webservices/.
[6]http://www.w3.org/
[7]靖红叶,基于Pi演算的Web服务组合的验证,[学位论文],太原,太原理工大学,2008,
[8]Microsoft Corporation. The Component Object Model Specification, October 1995,Draft Version 0.9.
[9] http://www.xml.org.cn/
[10]W3C. Web Services Description Language (WSDL) 1.2. http://www-w3.org/TR/wsdl/.
[11]贾志淳,基于Pi演算的Web服务组合兼容性验证方法研究,[学位论文],大连,大连海事大学,2008
[12]W3C. Simple Object Access Protocol (SOAP) 1.1. http://www.w3.org/TR/SOAP, 2001.
[13]Bob Atkinson,Giovanni Della-Libera, Satoshi Hada et al. Web Services Security (WS-Security) Version 1.005.Specifieation,April 2002.
[14]Hao He, Mark Potts, Lgor Sedukhin. Web Service Management: Service Life Cyele.W3C Working Group Note 11 February 2004.
[15]KangChan Lee, JongHong Jeon,Wonseok Lee, et al. QoS for Web Services: Requirements and Possible Approaches. W3C Working Group Note 25 November 2003.
[16]胡海涛,李刚,韩燕波,一种面向业务用户的大颗粒服务组合方法,计算机学报,2005(04),694-703
[17]5.Tsur, 5.Abiteboul,R. Agrawal, U. Dayal, J. Klein,and G. Weikum. Are Web Services the Next Revolution in e-Commerce? In Proceedings of the International Conference on Very Large Databases, Pages614一617, Roma, Italy, September 2001.
[18]张佩云,吴健,李莹,吴朝晖,基于回溯树的Web服务自动组合,软件学报,2007(08)
[19]F. Casati, M. Sayal, and M-C. Shan. Developing e-services for Composing Eservices. In Proceeding of 13th International Conference on Advanced information Systems Engineering (CAISE), Interlaken, Switzerland, June2001 Springer Verlag.
[20]F. Curbera, Y.Goland, J. Klein, F. Leymann, D. Roller, S. Thatte, S. Weerawarana. Business Process Exeeution language for Web services(Version1.0).IBM, July 2002.
[21]史玉良,Web服务合成的若干关键技术研究,[学位论文],上海,复旦大学2006
[22]Oasis: Business Process Execution Language for Web Services Specification. (2003), http://www-106.ibm.em/developerworks/library/ws-bpel.
[23]Business Process Execution Language for Web Services (BPEL), Version1.1. http://www.ibm.com/developerworks/library/ws-bpel, May 2003.
[24]BEA, IBM, Microsoft (2003), Business Process Execution Language for Web Services (BPEL4WS). http://xml.eoverpages.org/bpel4ws.html.
[25]W3C. Web Service Choreography Interface (WSCI) 1.0. http://www.w3.org/TR/wsei/2002.
[26]Business Process Execution Language for Web Services (BPEL), Version1.1. http://www.ibm.com/developerworks/library/ws-bpel, May 2003.
[27]UN/CEFACT and OASIS. ebXML Business Process Specification Schema (Version1.01). httP://ww.ebxml.org/specs/ebBPSS.Pdf, 2001.
[28]OASIS: ebXML-White Paper-Enabling Electronic Business with ebXML.(2000). http://www.ebxml.org/whitePapers/WhitePaper.htm .
[29] Business Process Modeling Language (BPML), http://www.bpmi.org .
[30] WFMC. Workflow Process Definition Interface-XML Process Definition Language http://www.wfme.org/standards/docs/TC-1025l0betaxpdl073002.pd, 2002 .
[31] R. Shapiro. A Comparison of XPDL, BPML and BPEL4WS. Accessed February 2003, http://xrnl.coverpages.org/Shapiro-XPDL.Pdf.
[32]J.Rao and X.Su, A Survey of Automated Web Service Composition Methods, In: proceedings of the First International Workshop on Semantic Web Services and Web Process Composition, 2004
[33]Joint US/EU ad hoc Agent Markup Language Committee. Reference description of the DAML+OIL ontology markup language. http://www.daml.org/2001/03/referenee, March 2001.
[34]http://www.mindswap.org/papers/SHOP2JWS.
[35]DAML Working Group. DARPA Annotated Markup Language. World Wide Web, http://www.daml.org,2003 .
[36]D Fensel, C Bussler1 The Web service modeling framework WSMF http://www.wsmo.org/papers/publications/wsmf.paper.pdf, 2004-05-18
[37] C. Wroe, R. Stevens, C. Goble, A. Roberts, and M. Greenwood, A Suite of DAML+OIL Ontologies to Describe Bioinformatics Web Services and Data. International Journal of Cooperative Information Systems, 12(2):197一224, 2003.
[38]Tanja Sollazzo, Siegfried Handschuh, Stenffen Staab, Martin R. Frank, Nenad Stojanovic: Semantic Web Service Architecture– Evolving Web Service Standards toward the Semantic Web. FLAIRS Conference 2002: 425-429
[39] W3C (2003) OWL Web Ontology Language overview. http://www.w3.org/TR /owl-features.
[40] Bert Robben, Frank Piessens, Wouter Joosen,Formalizing Correlate through the Pi-calculus,http://www.cs.kuleuven.ac.be/~distrinet/projects/CORRELATE/PUBLICATIONS/Models97. html 2007.
[41] John S. Davis, The Application of the Pi-Calculus to the Design of Embedded System, http://www.eees.berkeley.edu/IPRO/Summary/98abstraets/davisj.l.html, 2008.
[2]Web Services Description Language 1.2 www.w3.org/TR/wsdl
[3]http://uddi.org/pubs/uddi-v3.00-published-20020719.htm.
[4]Matskin, Mihhail, and Rao, Jinghai. Value-Added Web Services Composition Using Automatic Program Synthesis. Springer-Verlag Berlin Heidelberg, LNCS 2512, 2002, pp.213-224.
[5]IBM. IBM Web Services Tutorial. http://www-106.ibm.eom/develoPerworks/webservices/.
[6]http://www.w3.org/
[7]靖红叶,基于Pi演算的Web服务组合的验证,[学位论文],太原,太原理工大学,2008,
[8]Microsoft Corporation. The Component Object Model Specification, October 1995,Draft Version 0.9.
[9] http://www.xml.org.cn/
[10]W3C. Web Services Description Language (WSDL) 1.2. http://www-w3.org/TR/wsdl/.
[11]贾志淳,基于Pi演算的Web服务组合兼容性验证方法研究,[学位论文],大连,大连海事大学,2008
[12]W3C. Simple Object Access Protocol (SOAP) 1.1. http://www.w3.org/TR/SOAP, 2001.
[13]Bob Atkinson,Giovanni Della-Libera, Satoshi Hada et al. Web Services Security (WS-Security) Version 1.005.Specifieation,April 2002.
[14]Hao He, Mark Potts, Lgor Sedukhin. Web Service Management: Service Life Cyele.W3C Working Group Note 11 February 2004.
[15]KangChan Lee, JongHong Jeon,Wonseok Lee, et al. QoS for Web Services: Requirements and Possible Approaches. W3C Working Group Note 25 November 2003.
[16]胡海涛,李刚,韩燕波,一种面向业务用户的大颗粒服务组合方法,计算机学报,2005(04),694-703
[17]5.Tsur, 5.Abiteboul,R. Agrawal, U. Dayal, J. Klein,and G. Weikum. Are Web Services the Next Revolution in e-Commerce? In Proceedings of the International Conference on Very Large Databases, Pages614一617, Roma, Italy, September 2001.
[18]张佩云,吴健,李莹,吴朝晖,基于回溯树的Web服务自动组合,软件学报,2007(08)
[19]F. Casati, M. Sayal, and M-C. Shan. Developing e-services for Composing Eservices. In Proceeding of 13th International Conference on Advanced information Systems Engineering (CAISE), Interlaken, Switzerland, June2001 Springer Verlag.
[20]F. Curbera, Y.Goland, J. Klein, F. Leymann, D. Roller, S. Thatte, S. Weerawarana. Business Process Exeeution language for Web services(Version1.0).IBM, July 2002.
[21]史玉良,Web服务合成的若干关键技术研究,[学位论文],上海,复旦大学2006
[22]Oasis: Business Process Execution Language for Web Services Specification. (2003), http://www-106.ibm.em/developerworks/library/ws-bpel.
[23]Business Process Execution Language for Web Services (BPEL), Version1.1. http://www.ibm.com/developerworks/library/ws-bpel, May 2003.
[24]BEA, IBM, Microsoft (2003), Business Process Execution Language for Web Services (BPEL4WS). http://xml.eoverpages.org/bpel4ws.html.
[25]W3C. Web Service Choreography Interface (WSCI) 1.0. http://www.w3.org/TR/wsei/2002.
[26]Business Process Execution Language for Web Services (BPEL), Version1.1. http://www.ibm.com/developerworks/library/ws-bpel, May 2003.
[27]UN/CEFACT and OASIS. ebXML Business Process Specification Schema (Version1.01). httP://ww.ebxml.org/specs/ebBPSS.Pdf, 2001.
[28]OASIS: ebXML-White Paper-Enabling Electronic Business with ebXML.(2000). http://www.ebxml.org/whitePapers/WhitePaper.htm .
[29] Business Process Modeling Language (BPML), http://www.bpmi.org .
[30] WFMC. Workflow Process Definition Interface-XML Process Definition Language http://www.wfme.org/standards/docs/TC-1025l0betaxpdl073002.pd, 2002 .
[31] R. Shapiro. A Comparison of XPDL, BPML and BPEL4WS. Accessed February 2003, http://xrnl.coverpages.org/Shapiro-XPDL.Pdf.
[32]J.Rao and X.Su, A Survey of Automated Web Service Composition Methods, In: proceedings of the First International Workshop on Semantic Web Services and Web Process Composition, 2004
[33]Joint US/EU ad hoc Agent Markup Language Committee. Reference description of the DAML+OIL ontology markup language. http://www.daml.org/2001/03/referenee, March 2001.
[34]http://www.mindswap.org/papers/SHOP2JWS.
[35]DAML Working Group. DARPA Annotated Markup Language. World Wide Web, http://www.daml.org,2003 .
[36]D Fensel, C Bussler1 The Web service modeling framework WSMF http://www.wsmo.org/papers/publications/wsmf.paper.pdf, 2004-05-18
[37] C. Wroe, R. Stevens, C. Goble, A. Roberts, and M. Greenwood, A Suite of DAML+OIL Ontologies to Describe Bioinformatics Web Services and Data. International Journal of Cooperative Information Systems, 12(2):197一224, 2003.
[38]Tanja Sollazzo, Siegfried Handschuh, Stenffen Staab, Martin R. Frank, Nenad Stojanovic: Semantic Web Service Architecture– Evolving Web Service Standards toward the Semantic Web. FLAIRS Conference 2002: 425-429
[39] W3C (2003) OWL Web Ontology Language overview. http://www.w3.org/TR /owl-features.
[40] Bert Robben, Frank Piessens, Wouter Joosen,Formalizing Correlate through the Pi-calculus,http://www.cs.kuleuven.ac.be/~distrinet/projects/CORRELATE/PUBLICATIONS/Models97. html 2007.
[41] John S. Davis, The Application of the Pi-Calculus to the Design of Embedded System, http://www.eees.berkeley.edu/IPRO/Summary/98abstraets/davisj.l.html, 2008.