The rely/guarantee approach to verifying concurrent BPEL programs

Huibiao Zhu; Qiwen Xu; Chris Ma; Shengchao Qin; Zongyan Qiu

doi:10.1007/978-3-642-33826-7_12

The rely/guarantee approach to verifying concurrent BPEL programs

Huibiao Zhu^*
, Qiwen Xu
, Chris Ma
, Shengchao Qin
, Zongyan Qiu

^*Corresponding author for this work

Software Engineering Institute

University of Macau
Macao Polytechnic University
Teesside University
Peking University

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

1 Scopus citations

Abstract

Web services have become more and more important in these years, and BPEL4WS (BPEL) is the OASIS standard for web services composition and orchestration. It contains several distinct features, including scope-based compensation and fault handling mechanism. This paper focuses on the verification of BPEL programs, especially the verification of concurrent BPEL programs. The rely/guarantee approach is applied. Firstly, we present the operational semantics for BPEL programs. Secondly we apply the rely/guarantee method in the design of the verification rules. The rules can handle the features of BPEL programs, including compensation, fault handling and concurrency. Finally, the whole proof system is proved to be sound based on our operational semantics.

Original language	English
Title of host publication	Software Engineering and Formal Methods - 10th International Conference, SEFM 2012, Proceedings
Publisher	Springer Verlag
Pages	172-187
Number of pages	16
ISBN (Print)	9783642338250
DOIs	https://doi.org/10.1007/978-3-642-33826-7_12
State	Published - 2012
Event	10th International Conference on Software Engineering and Formal Methods, SEFM 2012 - Thessaloniki, Greece Duration: 1 Oct 2012 → 5 Oct 2012

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	7504 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	10th International Conference on Software Engineering and Formal Methods, SEFM 2012
Country/Territory	Greece
City	Thessaloniki
Period	1/10/12 → 5/10/12

Access to Document

10.1007/978-3-642-33826-7_12

Cite this

Zhu, H., Xu, Q., Ma, C., Qin, S., & Qiu, Z. (2012). The rely/guarantee approach to verifying concurrent BPEL programs. In Software Engineering and Formal Methods - 10th International Conference, SEFM 2012, Proceedings (pp. 172-187). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7504 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-642-33826-7_12

Zhu, Huibiao ; Xu, Qiwen ; Ma, Chris et al. / The rely/guarantee approach to verifying concurrent BPEL programs. Software Engineering and Formal Methods - 10th International Conference, SEFM 2012, Proceedings. Springer Verlag, 2012. pp. 172-187 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{ae3d807a7b4d4fd69827576a7c60c705,

title = "The rely/guarantee approach to verifying concurrent BPEL programs",

abstract = "Web services have become more and more important in these years, and BPEL4WS (BPEL) is the OASIS standard for web services composition and orchestration. It contains several distinct features, including scope-based compensation and fault handling mechanism. This paper focuses on the verification of BPEL programs, especially the verification of concurrent BPEL programs. The rely/guarantee approach is applied. Firstly, we present the operational semantics for BPEL programs. Secondly we apply the rely/guarantee method in the design of the verification rules. The rules can handle the features of BPEL programs, including compensation, fault handling and concurrency. Finally, the whole proof system is proved to be sound based on our operational semantics.",

author = "Huibiao Zhu and Qiwen Xu and Chris Ma and Shengchao Qin and Zongyan Qiu",

year = "2012",

doi = "10.1007/978-3-642-33826-7\_12",

language = "英语",

isbn = "9783642338250",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "172--187",

booktitle = "Software Engineering and Formal Methods - 10th International Conference, SEFM 2012, Proceedings",

address = "德国",

note = "10th International Conference on Software Engineering and Formal Methods, SEFM 2012 ; Conference date: 01-10-2012 Through 05-10-2012",

}

Zhu, H, Xu, Q, Ma, C, Qin, S & Qiu, Z 2012, The rely/guarantee approach to verifying concurrent BPEL programs. in Software Engineering and Formal Methods - 10th International Conference, SEFM 2012, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7504 LNCS, Springer Verlag, pp. 172-187, 10th International Conference on Software Engineering and Formal Methods, SEFM 2012, Thessaloniki, Greece, 1/10/12. https://doi.org/10.1007/978-3-642-33826-7_12

The rely/guarantee approach to verifying concurrent BPEL programs. / Zhu, Huibiao; Xu, Qiwen; Ma, Chris et al.
Software Engineering and Formal Methods - 10th International Conference, SEFM 2012, Proceedings. Springer Verlag, 2012. p. 172-187 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7504 LNCS).

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

TY - GEN

T1 - The rely/guarantee approach to verifying concurrent BPEL programs

AU - Zhu, Huibiao

AU - Xu, Qiwen

AU - Ma, Chris

AU - Qin, Shengchao

AU - Qiu, Zongyan

PY - 2012

Y1 - 2012

N2 - Web services have become more and more important in these years, and BPEL4WS (BPEL) is the OASIS standard for web services composition and orchestration. It contains several distinct features, including scope-based compensation and fault handling mechanism. This paper focuses on the verification of BPEL programs, especially the verification of concurrent BPEL programs. The rely/guarantee approach is applied. Firstly, we present the operational semantics for BPEL programs. Secondly we apply the rely/guarantee method in the design of the verification rules. The rules can handle the features of BPEL programs, including compensation, fault handling and concurrency. Finally, the whole proof system is proved to be sound based on our operational semantics.

AB - Web services have become more and more important in these years, and BPEL4WS (BPEL) is the OASIS standard for web services composition and orchestration. It contains several distinct features, including scope-based compensation and fault handling mechanism. This paper focuses on the verification of BPEL programs, especially the verification of concurrent BPEL programs. The rely/guarantee approach is applied. Firstly, we present the operational semantics for BPEL programs. Secondly we apply the rely/guarantee method in the design of the verification rules. The rules can handle the features of BPEL programs, including compensation, fault handling and concurrency. Finally, the whole proof system is proved to be sound based on our operational semantics.

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

U2 - 10.1007/978-3-642-33826-7_12

DO - 10.1007/978-3-642-33826-7_12

M3 - 会议稿件

AN - SCOPUS:84868221833

SN - 9783642338250

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 172

EP - 187

BT - Software Engineering and Formal Methods - 10th International Conference, SEFM 2012, Proceedings

PB - Springer Verlag

T2 - 10th International Conference on Software Engineering and Formal Methods, SEFM 2012

Y2 - 1 October 2012 through 5 October 2012

ER -

Zhu H, Xu Q, Ma C, Qin S, Qiu Z. The rely/guarantee approach to verifying concurrent BPEL programs. In Software Engineering and Formal Methods - 10th International Conference, SEFM 2012, Proceedings. Springer Verlag. 2012. p. 172-187. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-33826-7_12

The rely/guarantee approach to verifying concurrent BPEL programs

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this