BPEL2oWFN translates a web service expressed in WS-BPEL into a Petri net model.

The model can be used for computer-aided verification (model checking). Furthermore, the model can be used to

• synthesize a partner process, check for controllability, or generate the operating guideline using the analysis tool Fiona,
• check for deadlocks or any other Petri net property, or
• check any temporal logic formula with a variety of model checking tools.

Furthermore, 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.

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.

BPEL2oWFN was written by Niels Lohmann, Christian Gierds and Martin Znamirowski. It is part of the Tools4BPEL project funded by the Bundesministerium für Bildung und Forschung.

BPEL2oWFN can be downloaded as source code or pre-compiled for many operating systems.