| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 422213 | Electronic Notes in Theoretical Computer Science | 2008 | 23 Pages |
Abstract
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 π-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 π-based orchestration calculus and BPEL. This approach facilitates the verification and refinement process and may be applied to any BPEL implementation.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
