A Calculus for Generation, Verification and Refinement of BPEL Specifications

被引：19

作者：

Abouzaid, Faisal ^{[1
]}

Mullins, John ^{[1
]}

机构：

[1] Ecole Polytechn Montreal, CRAC Lab, Comp & Software Engn Dept, POB 6079, Montreal H3C 3P8, PQ, Canada

来源：

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2008年 / 200卷 / 03期

基金：

加拿大自然科学与工程研究理事会;

关键词：

Web services; orchestration; BPEL; formal methods; pi-calculus;

D O I：

10.1016/j.entcs.2008.04.092

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Business Process Execution Language for Web Services (WS-BPEL) is the emerging standard for designing Web Services compositions. In this context, formal methods can contribute to increased reliability and consistency in the BPEL design process. In this paper we propose an approach based on the HAL Toolkit that allows verification of the correctness of the behavior of a pi-based specification of interacting Web Services, and generates the BPEL processes that have the same behavior. This correlation based on two-way mapping between the pi-based orchestration calculus and BPEL. This approach facilitates the verification and refinement process and may be applied to any BPEL implementation.

引用

页码：43 / 65

页数：23

共 12 条

[1]

Alonso G., 2004, DAT SYS APP

[2]

Chirichiello A., 2005, 2005 IEEE WIC ACM IN

[3]

Ferrara A., 2004, ICSOC 04, P242, DOI DOI 10.1145/1035167.1035202

[4]

Ferrari G, 1997, LECT NOTES COMPUT SC, V1217, P275, DOI 10.1007/BFb0035394

[5]

Ferrari G., 2003, TECHNICAL REPORT

[6]

Lapadula A, 2007, LECT NOTES COMPUT SC, V4421, P33

[7]

Lapadula A, 2006, LECT NOTES COMPUT SC, V4038, P145

[8]

Lucchi R., 2007, J LOGIC ALGEBRAIC PR

[9]

Merro M, 1998, LECT NOTES COMPUT SC, V1443, P856, DOI 10.1007/BFb0055108

[10]

Milner R., 1993, MODAL LOGICS MOBILE

← 1 2 →