GNU BPEL2oWFN: 2.4 - from BPEL to Petri nets

GNU BPEL2oWFN translates a Web service expressed in WS-BPEL (Web Service
Business Process Execution Language) into a Petri net model. This model can be
used to:

- check for controllability or generate the operating guideline using the
  tools Fiona or Wendy,
- check for deadlocks or any other Petri net property, or
- check any temporal logic formula with a variety of model checking tools.

Furthermore, GNU BPEL2oWFN can translate a BPEL4Chor choreography to a Petri
net model. This model can be used to analyze properties of a complete
choreography or to synthesize a fitting service for an incomplete choreography.

GNU BPEL2oWFN uses static analysis to make the generated Petri net model as
compact as possible to analyze a chosen property. This is called flexible model
generation. Furthermore, several design flaws can be detected using control and
data flow analysis.