Tool support for BPEL verification in ActiveBPEL engine

Yi Qian; Yuming Xu; Zheng Wang; Geguang Pu; Huibiao Zhu; Chao Cai

doi:10.1109/ASWEC.2007.50

Tool support for BPEL verification in ActiveBPEL engine

Yi Qian^*, Yuming Xu, Zheng Wang, Geguang Pu, Huibiao Zhu, Chao Cai

^*Corresponding author for this work

Software Engineering Institute

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

22 Scopus citations

Abstract

The BPEL is designed for integrating and orches-trating web services and it provides the profound solution to model business process relying on web service platform. ActiveBPEL is a commercial-grade open source implementation engine for BPEL. In this paper, we describe the work on tool support for the BPEL verification in ActiveBPEL. We implement the algorithm of the mapping from BPEL to Timed Automata, and integrate it into the ActiveBPEL. By using model checker UPPAAL engine, ActiveBPEL is enhanced and can verify the BPEL properties, such as deadlock and reachability. Moreover, those timed properties of BPEL specification can be checked in our framework as well. Some case studies are presented to show the usage of verification functionality in ActiveBPEL.

Original language	English
Title of host publication	Proceedings - 2007 Australian Software Engineering Conference, ASWEC 2007 - Taming Complexity through Research and Practice
Pages	90-97
Number of pages	8
DOIs	https://doi.org/10.1109/ASWEC.2007.50
State	Published - 2007
Event	2007 Australian Software Engineering Conference, ASWEC 2007 - Taming Complexity through Research and Practice - Melbourne, Australia Duration: 10 Apr 2007 → 13 Apr 2007

Publication series

Name	Proceedings of the Australian Software Engineering Conference, ASWEC

Conference

Conference	2007 Australian Software Engineering Conference, ASWEC 2007 - Taming Complexity through Research and Practice
Country/Territory	Australia
City	Melbourne
Period	10/04/07 → 13/04/07

Keywords

ActiveBPEL
Timed automata
UPPAAL
Verification
WSBPEL
Workflow language

Access to Document

10.1109/ASWEC.2007.50

Cite this

Qian, Y., Xu, Y., Wang, Z., Pu, G., Zhu, H., & Cai, C. (2007). Tool support for BPEL verification in ActiveBPEL engine. In Proceedings - 2007 Australian Software Engineering Conference, ASWEC 2007 - Taming Complexity through Research and Practice (pp. 90-97). Article 4159662 (Proceedings of the Australian Software Engineering Conference, ASWEC). https://doi.org/10.1109/ASWEC.2007.50

@inproceedings{9da7919756c945e1918c8e057f8e699a,

title = "Tool support for BPEL verification in ActiveBPEL engine",

abstract = "The BPEL is designed for integrating and orches-trating web services and it provides the profound solution to model business process relying on web service platform. ActiveBPEL is a commercial-grade open source implementation engine for BPEL. In this paper, we describe the work on tool support for the BPEL verification in ActiveBPEL. We implement the algorithm of the mapping from BPEL to Timed Automata, and integrate it into the ActiveBPEL. By using model checker UPPAAL engine, ActiveBPEL is enhanced and can verify the BPEL properties, such as deadlock and reachability. Moreover, those timed properties of BPEL specification can be checked in our framework as well. Some case studies are presented to show the usage of verification functionality in ActiveBPEL.",

keywords = "ActiveBPEL, Timed automata, UPPAAL, Verification, WSBPEL, Workflow language",

author = "Yi Qian and Yuming Xu and Zheng Wang and Geguang Pu and Huibiao Zhu and Chao Cai",

year = "2007",

doi = "10.1109/ASWEC.2007.50",

language = "英语",

isbn = "0769527787",

series = "Proceedings of the Australian Software Engineering Conference, ASWEC",

pages = "90--97",

booktitle = "Proceedings - 2007 Australian Software Engineering Conference, ASWEC 2007 - Taming Complexity through Research and Practice",

note = "2007 Australian Software Engineering Conference, ASWEC 2007 - Taming Complexity through Research and Practice ; Conference date: 10-04-2007 Through 13-04-2007",

}

Qian, Y, Xu, Y, Wang, Z, Pu, G , Zhu, H & Cai, C 2007, Tool support for BPEL verification in ActiveBPEL engine. in Proceedings - 2007 Australian Software Engineering Conference, ASWEC 2007 - Taming Complexity through Research and Practice., 4159662, Proceedings of the Australian Software Engineering Conference, ASWEC, pp. 90-97, 2007 Australian Software Engineering Conference, ASWEC 2007 - Taming Complexity through Research and Practice, Melbourne, Australia, 10/04/07. https://doi.org/10.1109/ASWEC.2007.50

Tool support for BPEL verification in ActiveBPEL engine. / Qian, Yi; Xu, Yuming; Wang, Zheng et al.
Proceedings - 2007 Australian Software Engineering Conference, ASWEC 2007 - Taming Complexity through Research and Practice. 2007. p. 90-97 4159662 (Proceedings of the Australian Software Engineering Conference, ASWEC).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Tool support for BPEL verification in ActiveBPEL engine

AU - Qian, Yi

AU - Xu, Yuming

AU - Wang, Zheng

AU - Pu, Geguang

AU - Zhu, Huibiao

AU - Cai, Chao

PY - 2007

Y1 - 2007

N2 - The BPEL is designed for integrating and orches-trating web services and it provides the profound solution to model business process relying on web service platform. ActiveBPEL is a commercial-grade open source implementation engine for BPEL. In this paper, we describe the work on tool support for the BPEL verification in ActiveBPEL. We implement the algorithm of the mapping from BPEL to Timed Automata, and integrate it into the ActiveBPEL. By using model checker UPPAAL engine, ActiveBPEL is enhanced and can verify the BPEL properties, such as deadlock and reachability. Moreover, those timed properties of BPEL specification can be checked in our framework as well. Some case studies are presented to show the usage of verification functionality in ActiveBPEL.

AB - The BPEL is designed for integrating and orches-trating web services and it provides the profound solution to model business process relying on web service platform. ActiveBPEL is a commercial-grade open source implementation engine for BPEL. In this paper, we describe the work on tool support for the BPEL verification in ActiveBPEL. We implement the algorithm of the mapping from BPEL to Timed Automata, and integrate it into the ActiveBPEL. By using model checker UPPAAL engine, ActiveBPEL is enhanced and can verify the BPEL properties, such as deadlock and reachability. Moreover, those timed properties of BPEL specification can be checked in our framework as well. Some case studies are presented to show the usage of verification functionality in ActiveBPEL.

KW - ActiveBPEL

KW - Timed automata

KW - UPPAAL

KW - Verification

KW - WSBPEL

KW - Workflow language

UR - https://www.scopus.com/pages/publications/34548126438

U2 - 10.1109/ASWEC.2007.50

DO - 10.1109/ASWEC.2007.50

M3 - 会议稿件

AN - SCOPUS:34548126438

SN - 0769527787

SN - 9780769527789

T3 - Proceedings of the Australian Software Engineering Conference, ASWEC

SP - 90

EP - 97

BT - Proceedings - 2007 Australian Software Engineering Conference, ASWEC 2007 - Taming Complexity through Research and Practice

T2 - 2007 Australian Software Engineering Conference, ASWEC 2007 - Taming Complexity through Research and Practice

Y2 - 10 April 2007 through 13 April 2007

ER -

Tool support for BPEL verification in ActiveBPEL engine

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this