The Research on Formal Specification and Review of Workflows

The workflow technique based on BPEL is widely used in the management of enterprise business process. But it is hard to detect logic errors and conduct the validation of the business process, because BPEL does not have formal semantics. This paper introduces SOFL to describe business process. Generally speaking, SOFL provides a formal but comprehensible language for both requirements and design specifications, and a practical method for developing software systems. This paper extends SOFL to describe BPEL workflows and propose basic rules to transform BPEL into SOFL to demonstrate the ability of describing of SOFL. Then, an example is given to illustrate the rules. After that, this paper shows how to conduct the formal review of the SOFL module which is transformed from BPEL process, to ensure the internal consistency and validity of the business process.