Formal properties and analysis method of BPEL base on Petri net

Web service technologies based on service-oriented architecture (SOA) is becoming the key technology of the next generation business process. It is a significant issue to ensure a correct designing of business processes based on web services. Research on web service composition by means of formalized methods is necessary. Formal definition of Business Process Execution Language (BPEL) provides a complete description to reduce the inconsistency and ambiguity. This paper proposes a mapping from BPEL syntax elements to corresponding Petri net model and gives a formal definition of executable business process with corresponding formal model. We propose the BPEL formal model and properties systematically which include reachability, termination, replaceability, equivalence, receiving concurrency, sending concurrency, receiving conflict, link correctness and matching.