电子学报 ›› 2013, Vol. 41 ›› Issue (7): 1365-1370.DOI: 10.3969/j.issn.0372-2112.2013.07.019

• 学术论文 • 上一篇    下一篇

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

吉顺慧, 李必信, 邱栋   

  1. 东南大学计算机科学与工程学院, 江苏南京 211189
  • 收稿日期:2012-07-17 修回日期:2013-01-15 出版日期:2013-07-25
    • 作者简介:
    • 吉顺慧 女,1987年出生于江苏南通,现为东南大学计算机科学与工程学院在读博士,主要研究方向为Web服务组合分析、测试与验证.E-mail:shunhuiji@seu.edu.cn;李必信 男,1969年出生于安徽省庐江县,博士/博士后,现任东南大学计算机科学与工程学院教授、博士生导师,CCF高级会员,主要研究领域为软件分析、测试、验证,实证软件工程.E-mail:bx.li@seu.edu.cn邱栋 男,1986年出生于江苏海门,现为东南大学计算机科学与工程学院在读博士,主要研究方向为软件分析与测试.E-mail:dongqiu@seu.edu.cn
    • 基金资助:
    • 国家自然科学基金 (No.60973149); 博士点基金 (No.20100092110022); 江苏省高校科研成果产业化推进项目 (No.JHB2011-3);

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

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

  1. Department of Computer Science and Technology, Southeast University, Nanjing, Jiangsu 211189, China
  • Received:2012-07-17 Revised:2013-01-15 Online:2013-07-25 Published:2013-07-25

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

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

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.

Key words: Web service composition, extended control flow graph(XCFG), data flow property, verification

中图分类号: