A Calculus for Generation, Verification and Refinement of BPEL Specifications | Zendy

Faisal Abouzaid | Zendy; John Mullins | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

A Calculus for Generation, Verification and Refinement of BPEL Specifications

Author(s) -

Faisal Abouzaid,

John Mullins

Publication year - 2008

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2008.04.092

Subject(s) - business process execution language , computer science , correctness , orchestration , programming language , context (archaeology) , web service , consistency (knowledge bases) , process calculus , formal verification , software engineering , process (computing) , model checking , service oriented architecture , artificial intelligence , art , musical , paleontology , visual arts , biology

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

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research