Specifying and Verifying Business Process Models with Labeled Pi Calculus

Because of the strong expressive power and analysis capabilities, Pi calculus has been applied in the business process modeling area by more and more people. In existing works, Pi calculus is often used to capture the action execution logic of a business process. But the real situation is that some data and resource information are also critical for business process models besides action execution logic. Although it is possible to indirectly specify the behavior of data and resource with Pi processes, it is not intuitive for understanding and analyzing the holistic semantics of a business process. An extension for Pi calculus with state information, called labeled Pi calculus, is proposed in this paper. The main idea of labeled Pi calculus is to replace the abstract state name with the detailed state information, so that it can not only specify the semantics of action execution logic but also describe state transition of a business process. It can be regarded as an integrated formal method of state-based paradigm and event-based paradigm. Because state information is integrated to Pi calculus in a loosely coupled way, the theory and analysis capabilities of Pi calculus can be well-preserved in labeled Pi calculus. Moreover, new state simulation and equivalency relations are defined for labeled Pi calculus, which improve the analysis capability of Pi calculus considerably. A business process example is used to illustrate how to formalize the semantics of a business process with labeled Pi calculus and how to analyze the properties of it.

By: Ke Xu; Ying Liu; Cheng Wu

Published in: RC23606 in 2005


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 reports@us.ibm.com .