A model checking approach to verify BPEL4WS workflows

被引：14
|
作者：
Bianculli, Domenico [1 ]
Ghezzi, Carlo [2 ]
Spoletini, Paola [2 ]
机构：
[1] Univ Lugano, Fac Informat, Via G Buffi 13, CH-6900 Lugano, Switzerland
[2] Politecn Milan, Dipartimento Elettron & Informat, I-20133 Milan, Italy
来源：
IEEE INTERNATIONAL CONFERENCE ON SERVICE-ORIENTED COMPUTING AND APPLICATIONS, PROCEEDINGS | 2007年
关键词：
D O I：
10.1109/SOCA.2007.5
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
The increasing diffusion of service oriented computing in critical business transactions demands reliability and correctness of the workflow logic representing web service orchestrations. We present an approach for the formal verification of workflow-based compositions of web services, described in BPEL4WS. Workflow processes can be verified in isolation, assuming that the external services invoked are known only through their interface. It is also possible to verify that the actual composition of two or more processes behaves correctly. We can verify deadlock freedom, properties expressed as data-bound assertions written in WS-CoL, a specification language for web services, and LTL temporal properties. Our approach is based on the software model checker Bogon whose language supports the modeling of all BPEL4WS constructs. We provide an empirical evaluation of our approach and we compare the results with other BPEL4WS model checking tools.
引用
收藏
页码：13 / +
页数：3
相关论文
共 50 条
  • [21] BPEL4WS unit testing: Framework and implementation
    Li, ZH
    Sun, W
    Jiang, ZB
    Zhang, X
    2005 IEEE International Conference on Web Services, Vols 1 and 2, Proceedings, 2005, : 103 - 110
  • [22] A Model Checking Method to Verify BPEL4People Processes
    Bao, Fenye
    Zhang, Li
    2008 IEEE SYMPOSIUM ON ADVANCED MANAGEMENT OF INFORMATION FOR GLOBALIZED ENTERPRISES, PROCEEDINGS, 2008, : 106 - 110
  • [23] Agent negotiation based on BPEL4WS flow and constraints
    Chen, WF
    Liao, LJ
    Li, LC
    ICCC2004: Proceedings of the 16th International Conference on Computer Communication Vol 1and 2, 2004, : 1697 - 1702
  • [24] 基于BPEL4WS的Web服务合成
    邵志达
    范学峰
    微计算机应用, 2005, (06) : 76 - 78
  • [25] From DAML-S processes to BPEL4WS
    Liu, SS
    Khalaf, R
    Curbera, F
    14TH INTERNATIONAL WORKSHOP ON RESEARCH ISSUES ON DATA ENGINEERING: WEB SERVICES FOR E-COMMERCE AND E-GOVERNMENT APPLICATIONS, PROCEEDINGS, 2004, : 77 - 84
  • [26] Automated synthesis of composite BPEL4WS web services
    Pistore, M
    Traverso, P
    Bertoli, P
    Marconi, A
    2005 IEEE International Conference on Web Services, Vols 1 and 2, Proceedings, 2005, : 293 - 301
  • [27] Formal analysis of BPEL workflows with compensation by model checking
    Kovacs, Mate
    Varro, Daniel
    Goenczy, Laszlo
    COMPUTER SYSTEMS SCIENCE AND ENGINEERING, 2008, 23 (05): : 349 - 363
  • [28] Automating the provisioning of application services with the BPEL4WS workflow language
    Keller, A
    Badonnel, R
    UTILITY COMPUTING, 2004, 3278 : 15 - 27
  • [29] Metacomputing through the enactment of a BPEL4WS workflow in a grid environment
    Di Santo, M
    Ranaldo, N
    Zimeo, E
    ITCC 2005: INTERNATIONAL CONFERENCE ON INFORMATION TECHNOLOGY: CODING AND COMPUTING, VOL 1, 2005, : 316 - 321
  • [30] A method to extend BPEL4WS to enable business performance measurement
    McGregor, C
    ICWS'03: PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON WEB SERVICES, 2003, : 46 - 51
12345