微信服务号

微信订阅号

2025-4-24- 18
Home > Archive>Volume 23, Issue 3, 2012 >504-516. DOI:10.3724/SP.J.1001.2012.04065
PDF HTML XML Export Cite reminder
Path Sensitive Defect Analysis for BPEL Under Dead Path Semantic
Author:
Affiliation:

  • Article
    • | |
  • Metrics
    • |
  • Reference [26]
    • |
  • Related [20]
    • | | |
  • Comments
    Abstract:

    Software defect is an important indicator for measuring the adequacy of software testing. In order to improve the reliability and robustness of Web service composition based BPEL, this paper proposes a defect detecting method which combines the dead path into a path sensitive analysis. Dead path is a special semantic of BPEL, which has no execution information, but can connect two executed path segments. Using the abstract value of variable and its interval arithmetic, this method can identify an unreachable path and dead path, and also merge the conditions of property state at join points. A case study about uninitialized variable detecting which is related to dead path and executing path is given throughout the analysis, and verification is implemented to illustrate the effectiveness of this approach.

    Reference
    [1] Web services business process execution language Version 2.0. 2007. http://docs.oasis-open.org/wsbpel/2.0/OS/wsbpel-v2.0- OS.htm
    [2] Ferrara A. Webservices: A process algebra approach. In: Proc. of the 2nd Int’l Conf. on Service Oriented Computing. New York: ACM Press, 2004. 242-251. [doi: 10.1145/1035167.1035202]
    [3] Monakova G, Kopp O, Leymann F. Improving control flow verification in a business process using an extended Petri net. In: Proc. of the 1st Central-European Workshop on Services and their Composition (ZEUS 2009). 2009. 95-101.
    [4] Sun P, Jiang CJ. Analysis of workflow dynamic changes based on Petri net. Information and Software Technology, 2009,51(2): 284-292. [doi: 10.1016/j.infsof.2008.02.004]
    [5] Mukherjee A, Tari Z, Bertok P. Modeling of BPEL composite services using clustered coloured Petri-nets. In: Proc. of the World Conf. on Services—II. 2009. 55-62. [doi: 10.1109/SERVICES-2.2009.18]
    [6] Fisteus JA, Fernández LS, Kloos CD. Formal verification of BPEL4WS business collaborations. In: Proc. of the 5th Int’l Conf. on Electronic Commerce and Web Technologies (EC-Web 2004), Vol.80. 2004. 76-85. [doi: 10.1007/978-3-540-30077-9_8]
    [7] Foster H, Uchitel S, Magee J, Kramer J. Model-Based verification of Web service compositions. In: Proc. of the 18th IEEE Int’l Conf. on Automated Software Engineering. 2003. 152-161. [doi: 10.1109/ASE.2003.1240303]
    [8] Fu X, Bultan T, Su JW. Analysis of interacting BPEL Web services. In: Proc. of the 13th Int’l Conf. on World Wide Web. ACM Press, 2004. 621-630. [doi: 10.1145/988672.988756]
    [9] Lei LH, Duan ZH. An extended deterministic finite automata based method for the verification of composite Web services. Journal of Software, 2007,18(12):2980-2990 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/18/2980.htm [doi: 10. 1360/jos182980]
    [10] Wombacher A, Fankhauser P, Mahlek OB, Neuhold E. Matchmaking for business processes based on choreographies. In: Proc. of the 2004 IEEE Int’l Conf. on E-Technology, E-Commerce and E2 Service. Washington: IEEE Computer Society, 2004. 359-368.
    [11] Yang L, Liu X, Wang LZ, Chen X, Li XD. Scenario-Based analysis and verification for Web services message flows. Chinese Journal of Computers, 2009,32(9):1759-1772 (in Chinese with English abstract).
    [12] Zheng YY, Zhou J, Krause P. Analysis of BPEL data dependencies. In: Proc. of the 33rd EUROM ICRO Conf. on Software Engineering and Advanced Applications. Washington: IEEE Computer Society, 2007. 351-358. [doi: 10.1109/EUROMICRO.2007. 17]
    [13] Khalaf R, Kopp O, Leymann F. Maintaining data dependencies across BPEL process fragments. Int’l Journal of Cooperative Information Systems, 2008,17(3):259-282. [doi: 10.1142/S0218843008001828]
    [14] Yang XH, Huang JF, Gong YZ, Liu CC. Research on the static defect detecting in BPEL. Journal of Beijing University of Posts and Telecommunications, 2011,34(2):1-4 (in Chinese with English abstract).
    [15] van Breygel F, Koshkina M. Dead-Path-Elimination in BPEL4WS. In: Proc. of the 15th Int’l Conf. on Application of Concurrency to System Design (ACSD’05). 2005. 192-201. [doi: 10.1109/ACSD.2005.11].
    [16] Yang ZH, Gong YZ, Xiao Q, Wang YW. The application of interval computation in software testing based on defect pattern. Journal of Computer-aided Design & Computer Graphic, 2008,20(12):1630-1635 (in Chinese with English abstract).
    [17] Xiao Q, Gong YZ, Yang ZH, Jin DH, Wang YW. Path sensitive static defect detecting method. Journal of Software, 2010,21(2):209-217 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/3872.htm [doi: 10.3724/SP.J.1001.2010. 03872]
    [18] Das M, Lerner S, Seigle M. ESP: Path-Sensitive program verification in polynomial time. In: Knoop J, Hendren LJ, eds. Proc. of the ACM SIGPLAN Conf. on Programming Language Design and Implementation. New York: ACM Press, 2002. 57-68. [doi: 10. 1145/512529.512538]
    [19] Aho AV, Lam MS, Sethi R, Ullman JD. Compilers Principles, Techniques and Tools. 2nd ed., New York: Addison-Wesley, 2006. 626-632.
    [20] Ouyang C, Verbeek E, van der Aalst WMP, Breutel S, Dumas M, ter Hofstede AHM. Formal semantics and analysis of control flow in WS-BPE. In: Proc. of the Science of Computer Programming. Elsevier, 2007. 162-198. [doi: 10.1016/j.scico.2007.03.002]
    [21] Dong WL, Hu JH. Test method for BEPL-based Web service composition based on data flow analysis. Journal of Software, 2009, 20(8):2102-2112 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/568.htm [doi: 10.3724/SP.J.1001.2009. 00568]
    [22] Kopp O, Khalaf R, Leymann F. Reaching definitions analysis respecting dead path elimination semantics in BPEL processes. Technical Report, University Stuttgart, IAAS, 2007.
    [23] Kopp O, Khalaf R, Leymann F. Deriving explicit data links in WS-BPEL processes. In: Proc. of the IEEE SCC 2008. 2008. 367-376. [doi: 10.1109/SCC.2008.122]
    [24] Farahbod F, Glasser U, Vajihollahi M. Abstract operational semantics of the business process execution language for Web services. Technical Report, SFU-CMPT-TR-2004-03, Burnaby: School of Computer Science, Simon Fraser University, 2004.
    [25] Yang ZH, Gong YZ, Xiao Q, Wang YW. A defect model based testing system. Journal of Beijing University of Posts and Telecommunications, 2008,31(5):1-4 (in Chinese with English abstract).
    [26] Nakajima S. Model-Checking behavioral specification of BPEL applications. Electronic Notes in Theoretical Computer Science, 2006,151(2):89-105. [doi: 10.1016/j.entcs.2005.07.038]
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

杨学红,黄俊飞,宫云战.死路径语义下BPEL 路径敏感性缺陷分析.软件学报,2012,23(3):504-516

Copy
Share
Article Metrics
  • Abstract:4334
  • PDF: 5574
  • HTML: 0
  • Cited by: 0
History
  • Received:March 09,2011
  • Revised:May 06,2011
  • Online: March 05,2012
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2038183Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063