JI Shunhui, LI Bixin, QIU Dong. Incremental Verification of Evolving BPEL-Based Web Composite Service[J]. Chinese Journal of Electronics, 2016, 25(1): 6-12. doi: 10.1049/cje.2016.01.002
Citation: JI Shunhui, LI Bixin, QIU Dong. Incremental Verification of Evolving BPEL-Based Web Composite Service[J]. Chinese Journal of Electronics, 2016, 25(1): 6-12. doi: 10.1049/cje.2016.01.002

Incremental Verification of Evolving BPEL-Based Web Composite Service

doi: 10.1049/cje.2016.01.002
Funds:  This work is supported by Natural Science Foundation of Jiangsu Province (No.BK20140644) and Huawei Innovation Research Program (NO.YB2013120195).
  • Received Date: 2014-02-19
  • Rev Recd Date: 2014-06-10
  • Publish Date: 2016-01-10
  • Web composite services inevitably evolve to meet various requirements. However, most researchers only considered the verification of single versions. Simply reapplying the original verification techniques on subsequent versions of composite service as they evolve is costly, especially for large-scale services. In this paper, a new approach called Incremental verification (ICV) is proposed to incrementally verify the non-conflict property of evolved versions of Business process execution language (BPEL) based composite service. With a kind of eXtensible control flow graph (XCFG) as the formal model to describe the BPEL process, ICV compares the new version with the old one to identify the process changes which bring threats to the non-conflict property. Then it concentrates on the changed elements to perform the verification, which reduces the cost by skipping the analysis of unchanged elements. Case study shows that the proposed approach is effective and more efficient than the original verification method.
  • loading
  • A. Alves, A. Arkin, S. Askary, et al., “ASIS standard: Web services business process execution language version 2.0”, available at http://docs.oasis-open.org/wsbpel/2.0/, 2007-4.
    B. Li, S. Ji, D. Qiu, H. Leung and G. Zhang, “Verifying the concurrent properties in BPEL based web service composition process”, IEEE Transactions on Network and Service Management, Vol.10, No.4, pp.410-424, 2013.
    X. Fu, T. Bultan and J. Su, “WSAT: A tool for formal analysis of web services”, Proc. of International Conference on Computer Aided Verification, Boston, MA, USA, pp.510-514, 2004.
    R. Kazhamiakin, P. Pandya and M. Pistore, “Representation, verification, and computation of timed properties in web service compositions”, Proc. of IEEE International Conference on Web Services (ICWS), Chicago, IL, USA, pp.497-504, 2006.
    A. Ferrara, “Web services: A process algebra approach”, Proc. of International Conference on Service Oriented Computing, New York, USA, pp.242-251, 2004.
    Y. Feng and M. Kirchberg, “Verifying OWL-S service process models”, Proc. of 2011 IEEE International Conference on Web Service (ICWS), Washington, DC, USA, pp.307-324, 2011.
    S. Hinz, K. Schmidt and C. Stah, “Transforming BPEL to petrinets”, Proc. of 3rd International Conference on Business Process Management, Nancy, France, pp.220-235, 2005.
    C. Xu, W. Qu and H. Wang, “A Petri net-based method for data validation of web services composition”, Proc. of IEEE 34th Annual Computer Software and Applications Conference, Seoul, Korean, pp.468-476, 2010.
    N. Kokash and F. Arbab, “Formal design and verification of long-running transactions with extensible coordination tools”, IEEE Transaction on Services Computing, Vol.6, No.2, pp.186- 200, 2013.
    M. Graiet, I. Abbassi and L. Hamel, “Event-B based approach for verifying dynamic composite service transactional behavior”, Proc. of IEEE 20th International Conference on Web Services (ICWS), Santa Clara, CA, USA, pp.251-259, 2013.
    B. Godlin and O. Strichman, “Regression verification”, Proc. of 46th Design Automation Conference, San Francisco, CA, USA, pp.466-471, 2009.
    B. Godlin and O. Strichman, “Regression verification: Proving the equivalence of similar programs”, Software Testing, Verification and Reliability, Vol.23, No.3, pp.241-258, 2013.
    M. Bohme, B.C.D.S. Oliveira and A. Roychoudhury, “Partitionbased regression verification”, Proc. of 35th International Conference on Software Engineering (ICSE), San Francisco, CA, USA, pp.302-311, 2013.
    S. Chaki, N. Sharygina and N. Sinha, “Verification of evolving software”, Proc. of Specification and Verification of Computer- Based Systems, Newport Beach, CA, USA, pp.56-61, 2004.
    S. Chaki, E. Clarke, N. Sharygina and N. Sinha, “Verification of evolving software via component substitutability analysis”, Formal Methods in System Design, Vol.32, No.3, pp.235-266, 2008.
    G.W. Yang, M.B. Dwyer and G. Rothermel, “Regression model checking”, Proc. of IEEE International Conference on Software Maintenance, Edmonton, AB, Canada, pp.115-124, 2009.
    S. Ji, B. Li and D. Qiu, “XCFG-based analysis and verification for data flow property of BPEL”, Acta Electronica Sinica, Vol.41, No.7, pp.1365-1370, 2013. (in Chinese)
  • 加载中

Catalog

    通讯作者: 陈斌, bchen63@163.com
    • 1. 

      沈阳化工大学材料科学与工程学院 沈阳 110142

    1. 本站搜索
    2. 百度学术搜索
    3. 万方数据库搜索
    4. CNKI搜索

    Article Metrics

    Article views (195) PDF downloads(583) Cited by()
    Proportional views
    Related

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return