XCFG-Based Analysis and Verification for Data Flow Property of BPEL

JI Shun-hui; LI Bi-xin; QIU Dong

doi:10.3969/j.issn.0372-2112.2013.07.019

您当前的位置：

首页 >

文章列表页 >

XCFG-Based Analysis and Verification for Data Flow Property of BPEL

更新时间：2025-07-16

- XCFG-Based Analysis and Verification for Data Flow Property of BPEL
- Acta Electronica Sinica Vol. 41, Issue 7, Pages: 1365-1370(2013)
- 作者机构：
  
  东南大学计算机科学与工程学院,江苏,南京,211189
- 作者简介：
- 基金信息：
- DOI：10.3969/j.issn.0372-2112.2013.07.019
  CLC： TP311
- Published：2013
- 稿件说明：
移动端阅览
JI Shun-hui, LI Bi-xin, QIU Dong. XCFG-Based Analysis and Verification for Data Flow Property of BPEL[J]. Acta Electronica Sinica, 2013, 41(7): 1365-1370.
DOI：

JI Shun-hui, LI Bi-xin, QIU Dong. XCFG-Based Analysis and Verification for Data Flow Property of BPEL[J]. Acta Electronica Sinica, 2013, 41(7): 1365-1370. DOI： 10.3969/j.issn.0372-2112.2013.07.019.

摘要

BPEL组合服务实现了Web服务的复用和增值

但其复杂性带来了一定的挑战.例如

BPEL流程中正确的数据流对确保服务组合的正确性是十分重要的

然而现有的研究很少关注这类问题.本文提出一种基于扩展控制流图(XCFG)的BPEL流程数据流属性验证方法

利用XCFG对BPEL流程进行形式建模

设计相应的算法来分析和验证典型的数据流属性

如定义-使用一致性

无死锁和可达性.理论分析和实验均表明该方法是有效的.

Abstract

BPEL achieves reusability and value-adding of Web service through composing individual services.Meanwhile

it brings some challenges because of its complexity.For example

guaranteeing the data flow correct is very important for the correctness of BPEL process.However

few literatures focus on the data flow related analysis and verification.In this paper

we proposed an XCFG based technique

which models BPEL with XCFG and designs corresponding algorithms to analyze and verify the typical data flow property of BPEL

such as the consistency of define-use

deadlock-free and reachability.Both theoretical and experimental study validates the effectiveness of the XCFG based technique.

关键词

Keywords

references

Views

2032

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Inductive Verification of Powerlist-Based Carry Lookahead Adders

QoS-Aware Web Service Composition Based on Temporal Constraints Decomposition

Transforming HybridUML to Hybrid Program for CPS Property Verification

Bipoar Analog Integrated Circuit Computer Aided Dissection and Verification System

Related Author

任兴田

方娟

侯亚荣

代桂平

王勇

SONG Guo-xin

SHAO Zhi-qing

ZHANG Huan-huan

Related Institution

College of Computer Science & Technology,Beijing University of Technology

College of Electronic Information & Control Engineering,Beijing University of Technology

Institute of Computer Technology,East China University of Science and Technology

Laboratory of Computer Science,Institute of Software,Chinese Academy of Sciences

Institute of Computer TechnologyEast China University of Science and TechnologyShanghai 200237China

⁰