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

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

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. SEFM 2012
Editors	G. Eleftherakis , M Hinchey , M Holcombe
Publisher	Springer Berlin
ISBN (Electronic)	9783642338267
ISBN (Print)	9783642338250
DOIs	https://doi.org/10.1007/978-3-642-33826-7_12
Publication status	Published - 2012
Event	Software Engineering and Formal Methods - 10th International Conference - Thessaloniki, Greece Duration: 1 Oct 2012 → 5 Oct 2012 Conference number: 10

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer, Berlin
Volume	7504

Conference

Conference	Software Engineering and Formal Methods - 10th International Conference
Abbreviated title	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

@inproceedings{512a3b711f9e4defa51f7aff13492875,

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 = "English",

isbn = "9783642338250",

series = "Lecture Notes in Computer Science",

publisher = "Springer Berlin",

editor = "{Eleftherakis }, G. and {Hinchey }, M and {Holcombe }, M",

booktitle = "Software Engineering and Formal Methods. SEFM 2012",

address = "Germany",

note = "Software Engineering and Formal Methods - 10th International Conference, 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 G Eleftherakis , M Hinchey & M Holcombe (eds), Software Engineering and Formal Methods. SEFM 2012. Lecture Notes in Computer Science, vol. 7504, Springer Berlin, Software Engineering and Formal Methods - 10th International Conference, 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. SEFM 2012. ed. / G. Eleftherakis ; M Hinchey ; M Holcombe . Springer Berlin, 2012. (Lecture Notes in Computer Science; Vol. 7504).

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

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

N1 - Conference code: 10

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 - http://dx.doi.org/10.1007/978-3-642-33826-7_12

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

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

M3 - Conference contribution

SN - 9783642338250

T3 - Lecture Notes in Computer Science

BT - Software Engineering and Formal Methods. SEFM 2012

A2 - Eleftherakis , G.

A2 - Hinchey , M

A2 - Holcombe , M

PB - Springer Berlin

T2 - Software Engineering and Formal Methods - 10th International Conference

Y2 - 1 October 2012 through 5 October 2012

ER -

The Rely/Guarantee Approach to Verifying Concurrent BPEL Programs

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this