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

^*此作品的通讯作者

软件工程学院

University of Macau
Macao Polytechnic University
Teesside University
Peking University

科研成果: 书/报告/会议事项章节 › 会议稿件 › 同行评审

1 引用（Scopus）

摘要

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.

源语言	英语
主期刊名	Software Engineering and Formal Methods - 10th International Conference, SEFM 2012, Proceedings
出版商	Springer Verlag
页	172-187
页数	16
ISBN（印刷版）	9783642338250
DOI	https://doi.org/10.1007/978-3-642-33826-7_12
出版状态	已出版 - 2012
活动	10th International Conference on Software Engineering and Formal Methods, SEFM 2012 - Thessaloniki, 希腊期限: 1 10月 2012 → 5 10月 2012

丛书

姓名	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
卷	7504 LNCS
ISSN（印刷版）	0302-9743
ISSN（电子版）	1611-3349

会议

会议	10th International Conference on Software Engineering and Formal Methods, SEFM 2012
国家/地区	希腊
市	Thessaloniki
时期	1/10/12 → 5/10/12

访问文件

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

其它文件与链接

链接到 Scopus 的出版物

引用此

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

Zhu, Huibiao ; Xu, Qiwen ; Ma, Chris 等. / The rely/guarantee approach to verifying concurrent BPEL programs. Software Engineering and Formal Methods - 10th International Conference, SEFM 2012, Proceedings. Springer Verlag, 2012. 页码 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. 在 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), 卷 7504 LNCS, Springer Verlag, 页码 172-187, 10th International Conference on Software Engineering and Formal Methods, SEFM 2012, Thessaloniki, 希腊, 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 等.
Software Engineering and Formal Methods - 10th International Conference, SEFM 2012, Proceedings. Springer Verlag, 2012. 页码 172-187 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 卷 7504 LNCS).

科研成果: 书/报告/会议事项章节 › 会议稿件 › 同行评审

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. 在 Software Engineering and Formal Methods - 10th International Conference, SEFM 2012, Proceedings. Springer Verlag. 2012. 页码 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

摘要

丛书

会议

访问文件

其它文件与链接

学术指纹

引用此