基于XCFG的BPEL数据流属性分析与验证  

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

作　　者：吉顺慧[1] 李必信[1] 邱栋[1] 

机构地区：[1]东南大学计算机科学与工程学院,江苏南京211189

出　　处：《电子学报》2013年第7期1365-1370,共6页Acta Electronica Sinica

基　　金：国家自然科学基金(No.60973149);博士点基金(No.20100092110022);江苏省高校科研成果产业化推进项目(No.JHB2011-3)

摘　　要：BPEL组合服务实现了Web服务的复用和增值,但其复杂性带来了一定的挑战.例如,BPEL流程中正确的数据流对确保服务组合的正确性是十分重要的,然而现有的研究很少关注这类问题.本文提出一种基于扩展控制流图(XCFG)的BPEL流程数据流属性验证方法,利用XCFG对BPEL流程进行形式建模,设计相应的算法来分析和验证典型的数据流属性,如定义-使用一致性,无死锁和可达性.理论分析和实验均表明该方法是有效的.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.

关 键 词：WEB服务组合 扩展控制流图(XCFG) 数据流属性 验证 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]