Incremental Verification of Evolving BPEL-Based Web Composite Service

JI Shunhui; LI Bixin; QIU Dong

doi:10.1049/cje.2016.01.002

Volume 25 Issue 1

Turn off MathJax

Article Contents

Article Navigation > Chinese Journal of Electronics > 2016 > 25(1): 6-12

JI Shunhui, LI Bixin, QIU Dong, “Incremental Verification of Evolving BPEL-Based Web Composite Service,” Chinese Journal of Electronics, vol. 25, no. 1, pp. 6-12, 2016, doi: 10.1049/cje.2016.01.002

Citation:

JI Shunhui, LI Bixin, QIU Dong, “Incremental Verification of Evolving BPEL-Based Web Composite Service,” Chinese Journal of Electronics, vol. 25, no. 1, pp. 6-12, 2016, doi: 10.1049/cje.2016.01.002

Citation:

PDF( 557 KB)

Incremental Verification of Evolving BPEL-Based Web Composite Service

doi: 10.1049/cje.2016.01.002

JI Shunhui^1,2,
LI Bixin^1,2,
QIU Dong^1,2

1.
School of Computer Science and Engineering, Southeast University, Nanjing 211189, China;
2.
Key Laboratory of Computer Network and Information Integration (Southeast University), Ministry of Education, Nanjing 211189, China

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

Abstract

Abstract

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.
- Incremental verification,
- Evolution,
- Web composite service,
- eXtensible control flow graph (XCFG),
- Non-conflict property

FullText(HTML)

References(17)

References

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)

Relative Articles

Supplements(0)

Cited By

Proportional views