A Method of Transforming WS-BPEL2.0 to Extended Timed Automata Using Syntax Analyze Tree

Business Process Execution Language is an emerging standard language to describe web service composition behavior. With the emerging of BPEL, BPEL model checking is more and more important. There are many mathematical tools to model the behavior of BPEL process, and to help checking the model. This paper proposes a method to analyze WS-BPEL 2.0 process document and to transform it into extended timed automata. The analyzing of WS-BPEL process proposed in this paper is a unified approach and is easy executable. First, we use context-free-grammar to build syntax analyze tree of the WS-BPEL 2.0 process document. Then we simplify the tree, in order to remove redundant nodes and to make the structure more clearly. We design an extended timed automata which is called BPEL-ETA. BPEL-ETA can model activity with time constraints, it also taking data variables into consideration, so that data dependence can be detected during model checking. With the simplified tree, we build BPEL-ETA of the process. Then model checking tools can be used for the BPEL-ETA model, in this way, the WS-BPEL process model is checked. To realize our work, CPT system is built, which transforms WS-BPEL2.0 process to BPEL-ETA automatically.