| Residential College | false |
| Status | 已發表Published |
| The rely/guarantee approach to verifying concurrent BPEL programs | |
Zhu H.3; Xu Q.2 ; Ma C.5; Qin S.1; Qiu Z.4
| |
| 2012-11-06 | |
| Source Publication | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
 |
| ISSN | 03029743 16113349 |
| Volume | 7504 LNCSPages:172-187 |
| 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. © 2012 Springer-Verlag. |
| DOI | 10.1007/978-3-642-33826-7_12 |
| URL | View the original |
| Language | 英語English |
| Scopus ID | 2-s2.0-84868221833 |
| Fulltext Access | |
| Citation statistics | |
| Document Type | Journal article |
| Collection | DEPARTMENT OF COMPUTER AND INFORMATION SCIENCE |
| Affiliation | 1.University of Teesside 2.Universidade de Macau 3.East China Normal University 4.Peking University 5.Macau Polytechnic Institute |
| Recommended Citation GB/T 7714 | Zhu H.,Xu Q.,Ma C.,et al. The rely/guarantee approach to verifying concurrent BPEL programs[J]. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2012, 7504 LNCS, 172-187. |
| APA | Zhu H.., Xu Q.., Ma C.., Qin S.., & Qiu Z. (2012). The rely/guarantee approach to verifying concurrent BPEL programs. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 7504 LNCS, 172-187. |
| MLA | Zhu H.,et al."The rely/guarantee approach to verifying concurrent BPEL programs".Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 7504 LNCS(2012):172-187. |
| Files in This Item: | There are no files associated with this item. | |||||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment