GNU BPEL2oWFN 2.0.0
GNU BPEL2oWFN project translates a web service expressed in WS-BPEL into an oWFN.
· check for controllability or generate the operating guideline using the tool Fiona,
· check for deadlocks or any other Petri net property, or
· check any temporal logic formula with a variety of model checking tools.
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.