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

doi:10.3969/j.issn.0372-2112.2013.07.019

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

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

吉顺慧, 李必信, 邱栋

东南大学计算机科学与工程学院, 江苏南京 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

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

摘要/Abstract

摘要： 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

中图分类号:

TP311

吉顺慧, 李必信, 邱栋. 基于XCFG的BPEL数据流属性分析与验证[J]. 电子学报, 2013, 41(7): 1365-1370.

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.

参考文献

[1] Alves A,Arkin A,Askary S.Web services business process execution language version 2.0 [EB/OL].http://docs.oasis-open.org/wsbpel/20/OS/wsbpel-v2.0-OS.html.2007-4-11.
[2] Diaz G,Pardo J J,et al.Design and verification of web services compositions with timed automata[J].Electronic Notes in Theroretical Computer Science,2006,157(2):19-34.
[3] Cambronero M E,Diaz G,Valero V,et al.Validation and verification of web services choreographies by using timed automata[J].The Journal of Logic and Algebraic Programming,2011,80(1):25-49.
[4] Salaum G,Bordeaux L,Schaerf M.Describing and reasoing on web services using process algebra [A].Proceeding of IEEE International Conference on Web Servce [C].Washinton:IEEE Computer Society,2004.43-51.
[5] Peng Y,Ye L,Zheng Z,et al.Automatic service composition verification based on Pi-calculus [A].Proceeding of International Conference on E-Business and Information System Security [C].Wuhan:IEEE,2009.1-4.
[6] Hinz S,Schmidt K,Stah C.Transforming BPEL to petri-nets[J].Lecture Notes in Computer Science,2005,3649:220-235.
[7] Song W,Ma X.Ye,C,Dou W,Lu J.Timed modeling and verification of BPEL processed using timed Petri nets [A].Proceeding of the 9th International Conference on Quality Software [C].Cheju:IEEE,2009.92-97.
[8] Package org.apache.ode.bpel.compiler.bom [CP/OL].http://www.jarvana.com/javana/view/or/apache/ode-bpel-compiler/1.3.4/ode-bpel-compiler-1.3.4-javadoc.jar!/org/apache/od.
[9] 张功源.BPEL组合服务并发结构的分析与验证 [D].江苏南京:东南大学,2011.3. Zhang Gongyuan.Analysis and Verification of Concurrent Construct for BPEL-Based Service Composition [D].Nanjing,Jiangsu:Southeast University,2011,3.(in Chinese)
[10] Amighi A.Flow Graph Extraction for Modular Verification of Java Programs [D].Stockholm:KTH Royal Institute of Technology,2011.
[11] Kazhamiakin R,Pistore M.Static verification of control and data in web service compositions [A].Proceeding of IEEE International Conference on Web Services(ICWS'06) [C].Washington:IEEE Computer Society,2006.83-90.
[12] Moser S,Martens A,et al.Advanced verification of distributed WS-BPEL business processes incorporating CSSA-based data flow analysis [A].IEEE International Conference on Service Computing [C].Salt Lake City:IEEE,2007.98-105.
[13] Monakova G,Kopp O,et al.Verifying business rules using an SMT solver for BPEL processes [A].Proceedings of the Business Process and Services Computing Conference(BPSC'09) [C].Germany,2009.81-94.
[14] Yang X,Huang J,Gong Y.Static data flow analysis and anomalies detection for BPEL [A].Proceeding of International Conference on Test and Measurement(ICTM) [C].Hong Kong:IEEE,2009.18-21.
[15] Lei K,Zhang P.P,Lang B.Data access exception detecting of WS-BPEL process based on workflow nets [A].Proceding of International Conference on Computational Intelligence and Software Engineering(CiSE) [C].Wuhan:IEEE,2010.1-6.
[16] Xu C,Qu W,Wang,H,etc.A Petri net-based method for data validation of web services composition [A].Proceeding of 34th International Computer Software and Applications Conference [C].Seoul:IEEE,2010.468-476.
[17] 朱敏,李必信,等.基于微分动态逻辑的CPS建模和属性验证[J].电子学报,2012,40(6):1126-1132. Zhu Min,Li Bixin,et al.Transforming hybridUML to hybrid program for CPS property verification[J].Acta Electronica Sinica,2012,40(6):1126-1132.(in Chinese)

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

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

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

[1]	陈书仪, 刘亚丽, 林昌露, 李涛, 董永权. 面向物联网的轻量级可验证群组认证方案[J]. 电子学报, 2022, 50(4): 990-1001.
[2]	杨坤伟, 杨波, 周彦伟. 群智网络中基于区块链的有序聚合签名认证方案[J]. 电子学报, 2022, 50(2): 358-365.
[3]	蔡莹, 朱翔, 王舰, 李昊远, 韩建伟. 基于激光注入的FPGA加密防护设计验证研究[J]. 电子学报, 2022, 50(10): 2381-2386.
[4]	朱健, 胡凯, 张伯钧. 智能合约的形式化验证方法研究综述[J]. 电子学报, 2021, 49(4): 792-804.
[5]	杨启良, 周彦伟, 杨坤伟, 王涛. 标准模型下可公开验证的匿名IBE方案的安全性分析[J]. 电子学报, 2020, 48(2): 291-295.
[6]	房丙午, 黄志球, 王勇, 李勇. 状态不可观测的信息物理融合系统运行时验证[J]. 电子学报, 2018, 46(12): 2824-2831.
[7]	杜思军, 徐尚书, 刘俊南, 张俊伟, 马建峰. 云计算中抗共谋攻击的数据位置验证协议[J]. 电子学报, 2017, 45(6): 1321-1326.
[8]	叶恒舟, 李陶深, 关云慧. 基于时序约束分解的QoS感知的Web服务组合[J]. 电子学报, 2017, 45(5): 1150-1157.
[9]	任正伟, 孙小雁, 王丽娜, 王骞, 徐明迪, 张茂胜. 基于简单随机抽样的大数据可信性验证方法[J]. 电子学报, 2017, 45(10): 2484-2490.
[10]	彭巧, 田有亮. 基于多线性Diffie-Hellman问题的秘密共享方案[J]. 电子学报, 2017, 45(1): 200-205.
[11]	钱振江, 刘永俊, 姚宇峰, 汤力, 黄皓, 宋方敏. 微内核架构内存管理的形式化设计和验证方法研究[J]. 电子学报, 2017, 45(1): 251-256.
[12]	江南, 何炎祥, 张晓瞳. _mJava到Micro-Dalvik虚拟机的编译验证[J]. 电子学报, 2016, 44(7): 1619-1629.
[13]	李顺东, 杨坤伟, 巩林明, 毛庆, 刘新. 标准模型下可公开验证的匿名IBE方案[J]. 电子学报, 2016, 44(3): 673-678.
[14]	雷红轩, 彭家寅, 刘熠. 几类非确定型量子程序的终止验证[J]. 电子学报, 2016, 44(12): 2932-2938.
[15]	周洪丞, 杨超, 马建峰, 张俊伟. 云端数据异地容灾验证方案研究[J]. 电子学报, 2016, 44(10): 2485-2494.