Formalization, Verification and Restructuring of BPEL Models with Pi Calculus and Model Checking

BPEL (Business Process Executable Language for Web Services) is an emerging standard for business application integration and B2B processing based on web services. As a popular specification for modeling and implementing business processes, building reliable and secure business application systems with BPEL becomes an important issue. In this work, BPEL models are automatically verified and analyzed with our Open Process AnaLyzer (OPAL) toolkit by formally capturing BPEL’s semantics in Pi Calculus. The contribution of the work can be concluded in four points. First, the semantics of BPEL is fully formalized with Pi calculus; Second, the soundness of the formalization is validated and important properties are proved to be preserved in the formalization. Third, a concrete scenario is illustrated to show how model checking is applied to verify the reliability of BPEL model designs. Last, equivalence analysis in Pi calculus and model checking are combined to implement restructuring algorithms by which a BPEL model can be restructured for performance enhancement with OPAL.

By: Ke Xu; Ying Liu; Geguang Pu

Published in: RC23962 in 2006


This Research Report is available. This report has been submitted for publication outside of IBM and will probably be copyrighted if accepted for publication. It has been issued as a Research Report for early dissemination of its contents. In view of the transfer of copyright to the outside publisher, its distribution outside of IBM prior to publication should be limited to peer communications and specific requests. After outside publication, requests should be filled only by reprints or legally obtained copies of the article (e.g., payment of royalties). I have read and understand this notice and am a member of the scientific community outside or inside of IBM seeking a single copy only.


Questions about this service can be mailed to .