Path Feasibility Analysis of BPEL Processes under Dead Path Elimination Semantics

DOI Web Site 参考文献22件
  • WANG Hongda
    College of Defense Engineering, PLA University of Science and Technology
  • XING Jianchun
    College of Defense Engineering, PLA University of Science and Technology
  • LI Juelong
    Technical Management Office of Naval Defense Engineering
  • YANG Qiliang
    College of Defense Engineering, PLA University of Science and Technology
  • ZHANG Xuewei
    College of Defense Engineering, PLA University of Science and Technology
  • HAN Deshuai
    College of Defense Engineering, PLA University of Science and Technology
  • LI Kai
    State Grid Xinjiang Information and Telecommunication Company

抄録

Web Service Business Process Execution Language (BPEL) has become the de facto standard for developing instant service-oriented workflow applications in open environment. The correctness and reliability of BPEL processes have gained increasing concerns. However, the unique features (e.g., dead path elimination (DPE) semantics, parallelism, etc.) of BPEL language have raised enormous problems to it, especially in path feasibility analysis of BPEL processes. Path feasibility analysis of BPEL processes is the basis of BPEL testing, for it relates to the test case generation. Since BPEL processes support both parallelism and DPE semantics, existing techniques can't be directly applied to its path feasibility analysis. To address this problem, we present a novel technique to analyze the path feasibility for BPEL processes. First, to tackle unique features mentioned above, we transform a BPEL process into an intermediary model — BPEL control flow graph, which is proposed to abstract the execution flow of BPEL processes. Second, based on this abstraction, we symbolically encode every path of BPEL processes as some Satisfiability formulas. Finally, we solve these formulas with the help of Satisfiability Modulo Theory (SMT) solvers and the feasible paths of BPEL processes are obtained. We illustrate the applicability and feasibility of our technique through a case study.

収録刊行物

参考文献 (22)*注記

もっと見る

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ