A Feature-Complete Petri Net Semantics for WS-BPEL 2.0 and Its Compiler BPEL2oWFN
Recently, the emerging standard to describe business processes on top of Web service technology, the Web Service Business Execution Language (WS-BPEL), has been officially specified. The authors present an extension of a Petri net semantics for the Web Service Business Execution Language (WS-BPEL). This extension covers the novel activities and constructs introduced by the recent WS-BPEL 2.0 specification. Furthermore, they simplify several aspects of the Petri net semantics to allow for more compact models suited for computer-aided verification.