Path Feasibility Analysis of BPEL Processes under Dead Path Elimination Semantics

Hongda WANG; Jianchun XING; Juelong LI; Qiliang YANG; Xuewei ZHANG; Deshuai HAN; Kai LI

doi:10.1587/transinf.2015EDP7121

Path Feasibility Analysis of BPEL Processes under Dead Path Elimination Semantics

Hongda WANG, Jianchun XING, Juelong LI, Qiliang YANG, Xuewei ZHANG, Deshuai HAN, Kai LI

Full Text Views

0

Share
Cite this

Summary :

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.

Publication: IEICE TRANSACTIONS on Information Vol.E99-D No.3 pp.641-649

Publication Date: 2016/03/01

Publicized: 2015/11/27

Online ISSN: 1745-1361

DOI: 10.1587/transinf.2015EDP7121

Type of Manuscript: PAPER

Category: Software Engineering

Authors

Hongda WANG
  PLA University of Science and Technology
Jianchun XING
  PLA University of Science and Technology
Juelong LI
  Technical Management Office of Naval Defense Engineering
Qiliang YANG
  PLA University of Science and Technology
Xuewei ZHANG
  PLA University of Science and Technology
Deshuai HAN
  PLA University of Science and Technology
Kai LI
  State Grid Xinjiang Information and Telecommunication Company

Keyword

BPEL processes, path feasibility analysis, dead path elimination, BPEL control flow graph, SMT solver

Cite this

Copy

Hongda WANG, Jianchun XING, Juelong LI, Qiliang YANG, Xuewei ZHANG, Deshuai HAN, Kai LI, "Path Feasibility Analysis of BPEL Processes under Dead Path Elimination Semantics" in IEICE TRANSACTIONS on Information, vol. E99-D, no. 3, pp. 641-649, March 2016, doi: 10.1587/transinf.2015EDP7121.
Abstract: 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.
URL: https://globals.ieice.org/en_transactions/information/10.1587/transinf.2015EDP7121/_p

Copy

@ARTICLE{e99-d_3_641,
author={Hongda WANG, Jianchun XING, Juelong LI, Qiliang YANG, Xuewei ZHANG, Deshuai HAN, Kai LI, },
journal={IEICE TRANSACTIONS on Information},
title={Path Feasibility Analysis of BPEL Processes under Dead Path Elimination Semantics},
year={2016},
volume={E99-D},
number={3},
pages={641-649},
abstract={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.},
keywords={},
doi={10.1587/transinf.2015EDP7121},
ISSN={1745-1361},
month={March},}

Copy

TY - JOUR
TI - Path Feasibility Analysis of BPEL Processes under Dead Path Elimination Semantics
T2 - IEICE TRANSACTIONS on Information
SP - 641
EP - 649
AU - Hongda WANG
AU - Jianchun XING
AU - Juelong LI
AU - Qiliang YANG
AU - Xuewei ZHANG
AU - Deshuai HAN
AU - Kai LI
PY - 2016
DO - 10.1587/transinf.2015EDP7121
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E99-D
IS - 3
JA - IEICE TRANSACTIONS on Information
Y1 - March 2016
AB - 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.
ER -