| 3 |
|
|
| 4 |
About this document: |
About this document: |
| 5 |
|
|
| 6 |
This manual is for GNU BPEL2oWFN, version 2.0.1, a tool translating |
This manual is for GNU BPEL2oWFN, version 2.0.2, a tool translating |
| 7 |
a BPEL process into an open workflow net (oWFN), last updated 11 May |
a BPEL process into an open workflow net (oWFN), last updated 15 June |
| 8 |
2007. |
2007. |
| 9 |
|
|
| 10 |
Copyright (C) 2005, 2006, 2007 Niels Lohmann |
Copyright (C) 2005, 2006, 2007 Niels Lohmann |
| 67 |
* check any temporal logic formula with a variety of model checking |
* check any temporal logic formula with a variety of model checking |
| 68 |
tools. |
tools. |
| 69 |
|
|
| 70 |
|
Furthermore, BPEL2oWFN can translate a BPEL4Chor choreography to a |
| 71 |
|
Petri net model. This model can be used to analyze properties of a |
| 72 |
|
complete choreography or to synthesize a fitting service for an |
| 73 |
|
incomplete choreography. |
| 74 |
|
|
| 75 |
BPEL2oWFN uses static analysis to make the generated Petri net model as |
BPEL2oWFN uses static analysis to make the generated Petri net model as |
| 76 |
compact as possible to analyze a chosen property. This is called |
compact as possible to analyze a chosen property. This is called |
| 77 |
flexible model generation. Furthermore, several design flaws can be |
flexible model generation. Furthermore, several design flaws can be |
| 122 |
|
|
| 123 |
The standard invocation of BPEL2oWFN is: |
The standard invocation of BPEL2oWFN is: |
| 124 |
|
|
| 125 |
bpel2owfn -i service.bpel -f owfn -o |
bpel2owfn -i service.bpel -m petrinet -f owfn -o |
| 126 |
|
|
| 127 |
where `service.bpel' is a BPEL process. The option `-f owfn' causes |
where `service.bpel' is a BPEL process. The option `-f owfn' causes |
| 128 |
BPEL2oWFN to generate an open workflow net. This net is written to a |
BPEL2oWFN to generate an open workflow net (option `-m petrinet'). This |
| 129 |
file named `service.owfn', because of the option `-o'. |
net is written to a file named `service.owfn', because of the option |
| 130 |
|
`-o'. |
| 131 |
|
|
| 132 |
BPEL2oWFN can be called without any parameter. In this case, it acts as |
BPEL2oWFN can be called without any parameter. In this case, it acts as |
| 133 |
a simple parser for BPEL processes that reads its input from the |
a simple parser for BPEL processes that reads its input from the |
| 149 |
`--input=FILENAME.bpel' |
`--input=FILENAME.bpel' |
| 150 |
`-i FILENAME.bpel' |
`-i FILENAME.bpel' |
| 151 |
Read a BPEL process from file `FILENAME.bpel'. If this parameter |
Read a BPEL process from file `FILENAME.bpel'. If this parameter |
| 152 |
is omitted, input is read from standard input (`stdin'). |
is omitted, input is read from standard input (`stdin'). Wildcards |
| 153 |
|
such as `process*.bpel' are also allowed. |
| 154 |
|
|
| 155 |
|
`--wsdl=FILENAME.wsdl' |
| 156 |
|
`-w FILENAME.wsdl' |
| 157 |
|
Read a WSDL file to support the translation. |
| 158 |
|
|
| 159 |
|
`--topology=FILENAME.xml' |
| 160 |
|
`-t FILENAME.xml' |
| 161 |
|
Read a BPEL4Chor participant topology file to support the |
| 162 |
|
translation of BPEL4Chor choreographies. Can only be used with the |
| 163 |
|
`choreography' mode. |
| 164 |
|
|
| 165 |
`--output[=FILENAME]' |
`--output[=FILENAME]' |
| 166 |
`-o' |
`-o' |
| 218 |
`--reduce=0-5' |
`--reduce=0-5' |
| 219 |
`-r 0-5' |
`-r 0-5' |
| 220 |
Apply several structural reduction rules to the generated Petri |
Apply several structural reduction rules to the generated Petri |
| 221 |
net model (implies mode `petrinet' or `consistency'). The rules |
net model (implies mode `petrinet' or `choreography'). The rules |
| 222 |
preserve deadlocks, livelocks and all deadlock-free communicating |
preserve deadlocks, livelocks and all deadlock-free communicating |
| 223 |
partners. The rules are organized in reduction levels: |
partners. The rules are organized in reduction levels: |
| 224 |
|
|
| 275 |
Furthermore, faulty constellations such as conflicting |
Furthermore, faulty constellations such as conflicting |
| 276 |
receiving activities can be found using the `cfg' mode. |
receiving activities can be found using the `cfg' mode. |
| 277 |
|
|
| 278 |
`consistency' |
`choreography' |
| 279 |
The `consistency' mode is an extension of the `petrinet' |
The `choreography' mode(1) is an extension of the `petrinet' |
| 280 |
mode. In the consistency mode, several BPEL processes can be |
mode. In the choreography mode, several BPEL processes can be |
| 281 |
parsed, and a Petri net model of their composition is |
parsed, and a Petri net model of their composition is |
| 282 |
generated. |
generated. |
| 283 |
|
|
| 284 |
The `consistency' mode is in beta stage. It is not fully |
For examples, check `test/bpel4chor' directory. When |
| 285 |
tested. For examples, check the `test5' test script in the |
combined with LoLA file output, an additional `.task' file is |
| 286 |
`tests' directory. When combined with LoLA file output, an |
generated. With the help of this file LoLA can check for weak |
| 287 |
additional `.task' file is generated. With the help of this |
termination of the composition. |
| 288 |
file LoLA can check for weak termination of the composition. |
|
| 289 |
|
Note that the choreography mode is only tested with the |
| 290 |
|
`small' mode. To support the translation of a BPEL4Chor |
| 291 |
|
choreography, a participant topology can be additionally |
| 292 |
|
parsed using the `topology' parameter. |
| 293 |
|
|
| 294 |
`petrinet' |
`petrinet' |
| 295 |
Generates a Petri net representing the semantics of the given |
Generates a Petri net representing the semantics of the given |
| 315 |
`--parameter=PAR' |
`--parameter=PAR' |
| 316 |
`-p PAR' |
`-p PAR' |
| 317 |
|
|
| 318 |
`communicationonly' |
`small' |
| 319 |
Only the communicational behavior of the input BPEL process is |
With the `small' parameter(2), only the communicational |
| 320 |
modeled. That is, the negative control flow (fault, |
behavior of the input BPEL process is modeled. That is, the |
| 321 |
termination, or compensation handlers, as well as `<exit>', |
negative control flow (fault, termination, or compensation |
| 322 |
`<throw>', `<compensate>', `<compensateScope>' activities) is |
handlers, as well as `<exit>', `<throw>', `<compensate>', |
| 323 |
not translated to the Petri net model. When combined with |
`<compensateScope>' activities) is not translated to the |
| 324 |
`reduce', this parameter yields the most compact Petri net |
Petri net model. When combined with `reduce', this parameter |
| 325 |
model. |
yields the most compact Petri net model. |
| 326 |
|
|
| 327 |
`fhfaults' |
`fhfaults' |
| 328 |
Confines the `standardfaults' parameter: in the negative |
Confines the `standardfaults' parameter: in the negative |
| 372 |
files together since XML requires the mode `pretty', whereas LoLA |
files together since XML requires the mode `pretty', whereas LoLA |
| 373 |
requires the mode `petrinet'. |
requires the mode `petrinet'. |
| 374 |
|
|
| 375 |
Petri net file formats (imply mode `petrinet' or `consistency'): |
Petri net file formats (imply mode `petrinet' or `choreography'): |
| 376 |
|
|
| 377 |
`apnn' |
`apnn' |
| 378 |
Outputs the inner of the generated open workflow net in |
Outputs the inner of the generated open workflow net in |
| 412 |
net output format that outputs the complete open |
net output format that outputs the complete open |
| 413 |
workflow net, that is, also the interface is exported. |
workflow net, that is, also the interface is exported. |
| 414 |
Currently, the interface places are annotated using a |
Currently, the interface places are annotated using a |
| 415 |
`<type>' tag which is only supported by Yasper(1). When |
`<type>' tag which is only supported by Yasper(3). When |
| 416 |
the parameter `-o' is used, a file with the suffix |
the parameter `-o' is used, a file with the suffix |
| 417 |
`.pnml' is created. |
`.pnml' is created. |
| 418 |
|
|
| 483 |
In this section we show some examples how BPEL2oWFN can be invoked. See |
In this section we show some examples how BPEL2oWFN can be invoked. See |
| 484 |
*Note File Formats:: for more examples. |
*Note File Formats:: for more examples. |
| 485 |
|
|
| 486 |
`bpel2owfn -i sample.bpel -flola -finfo -o -p reduce' |
`bpel2owfn -i sample.bpel -m petrinet -f lola -f info -o -p reduce' |
| 487 |
Reads the file `sample.bpel', generates a structural reduced |
Reads the file `sample.bpel', generates a structural reduced |
| 488 |
low-level Petri net and saves it in a LoLA file `sample.lola'. For |
low-level Petri net and saves it in a LoLA file `sample.lola'. For |
| 489 |
further information a file `sample.info' is generated. |
further information a file `sample.info' is generated. |
| 490 |
|
|
| 491 |
`bpel2owfn -i sample.bpel -fowfn -d3 -o' |
`bpel2owfn -i sample.bpel -mpetrinet -fowfn -d3 -o' |
| 492 |
Reads the file `sample.bpel', generates a low-level open workflow |
Reads the file `sample.bpel', generates a low-level open workflow |
| 493 |
net and saves it in an oWFN file `sample.owfn'. For further |
net and saves it in an oWFN file `sample.owfn'. For further |
| 494 |
information a file `sample.info' is generated. During the |
information a file `sample.info' is generated. During the |
| 504 |
Reads the file `sample.bpel' and prints the abstract syntax tree |
Reads the file `sample.bpel' and prints the abstract syntax tree |
| 505 |
(AST) to standard output. |
(AST) to standard output. |
| 506 |
|
|
| 507 |
`bpel2owfn -m consistency -i service1.bpel -i service2.bpel -f lola -o' |
`bpel2owfn -m choreography -i service1.bpel -i service2.bpel -f lola -o' |
| 508 |
Reads the files `service1.bpel' and `service2.bpel' and creates a |
Reads the files `service1.bpel' and `service2.bpel' and creates a |
| 509 |
Petri net model of their composition. The result is written to the |
Petri net model of their composition. The result is written to the |
| 510 |
LoLA file `service1_service2.lola'. Furthermore, an analysis file |
LoLA file `service1_service2.lola'. Furthermore, an analysis file |
| 511 |
`service1_service2.task' is written that can be processed by LoLA. |
`service1_service2.task' is written that can be processed by LoLA. |
| 512 |
|
|
| 513 |
|
Further examples for invocations of BPEL2oWFN can be found in the |
| 514 |
|
`tests' directory of the source distribution. |
| 515 |
|
|
| 516 |
---------- Footnotes ---------- |
---------- Footnotes ---------- |
| 517 |
|
|
| 518 |
(1) Yasper is available at `http://www.yasper.org'. |
(1) This mode was formally called `consinstency'. |
| 519 |
|
|
| 520 |
|
(2) This mode was formally called `communicationonly'. |
| 521 |
|
|
| 522 |
|
(3) Yasper is available at `http://www.yasper.org'. |
| 523 |
|
|
| 524 |
3 Warnings and Error Messages |
3 Warnings and Error Messages |
| 525 |
***************************** |
***************************** |
| 843 |
abstract process are reported as warnings. |
abstract process are reported as warnings. |
| 844 |
116 notice An `<opaqueActivity>' of an abstract process is |
116 notice An `<opaqueActivity>' of an abstract process is |
| 845 |
modeled by an `<empty>' activity. |
modeled by an `<empty>' activity. |
| 846 |
117 notice When using the parameter `communicationonly', the |
117 notice When using the parameter `small', the occurrence of |
| 847 |
occurrence of join failures is not modeled. Thus, any |
join failures is not modeled. Thus, any activity is |
| 848 |
activity is treated as if the attribute |
treated as if the attribute `suppressJoinFailure' is |
| 849 |
`suppressJoinFailure' is set to `yes'.(8) |
set to `yes'.(8) |
| 850 |
118 notice A user-defined transition condition is ignored and |
118 notice A user-defined transition condition is ignored and |
| 851 |
modeled as "n-out-of-n" (`true') instead. |
modeled as "n-out-of-n" (`true') instead. |
| 852 |
119 notice A user-defined transition condition is ignored and |
119 notice A user-defined transition condition is ignored and |
| 853 |
modeled as "1-out-of-n" (XOR) instead. |
modeled as "1-out-of-n" (XOR) instead. |
| 854 |
120 notice When using the parameter `communicationonly', the FTC |
120 notice When using the parameter `small', the FTC (fault, |
| 855 |
(fault, termination, and compensation) handlers are |
termination, and compensation) handlers are not |
| 856 |
not modeled. |
modeled. |
| 857 |
121 notice When using the parameter `communicationonly', |
121 notice When using the parameter `small', activities of the |
| 858 |
activities of the negative control flow (`<exit>', |
negative control flow (`<exit>', `<throw>', |
| 859 |
`<throw>', `<compensate>', and `<compensateScope>') |
`<compensate>', and `<compensateScope>') are replaced |
| 860 |
are replaced by an `<empty>' activity. |
by an `<empty>' activity. |
| 861 |
122 notice A syntax error in the BPEL4Chor chorography file |
122 notice A syntax error in the BPEL4Chor chorography file |
| 862 |
occurred. |
occurred. |
| 863 |
123 notice A syntax error in the WSDL input file occurred. |
123 notice A syntax error in the WSDL input file occurred. |
| 898 |
for a `<participant>'. In a WS-BPEL file, the |
for a `<participant>'. In a WS-BPEL file, the |
| 899 |
attribute `targetNamespace' could not to be grounded |
attribute `targetNamespace' could not to be grounded |
| 900 |
to a BPEL4Chor `<participant>'. |
to a BPEL4Chor `<participant>'. |
| 901 |
|
138 notice In a BPEL4Chor topology, a partner link specified for |
| 902 |
|
an activity was not found. Instead, the name of the |
| 903 |
|
specified id is used as a partner link. |
| 904 |
|
|
| 905 |
---------- Footnotes ---------- |
---------- Footnotes ---------- |
| 906 |
|
|
| 1027 |
`id') was added to every activity. |
`id') was added to every activity. |
| 1028 |
|
|
| 1029 |
We now want to create a compact Petri net model of the BPEL process, |
We now want to create a compact Petri net model of the BPEL process, |
| 1030 |
using the `petrinet' mode and the `communicationonly' parameter: |
using the `petrinet' mode and the `small' parameter: |
| 1031 |
|
|
| 1032 |
bpel2owfn -i example.bpel -m petrinet -p communicationonly |
bpel2owfn -i example.bpel -m petrinet -p small |
| 1033 |
|
|
| 1034 |
BPEL2oWFN now also displays statistics of the generated Petri net model: |
BPEL2oWFN now also displays statistics of the generated Petri net model: |
| 1035 |
|
|
| 1039 |
input and one output place, two transitions and six arcs. To create a |
input and one output place, two transitions and six arcs. To create a |
| 1040 |
graphical representation, invoke BPEL2oWFN with the following options: |
graphical representation, invoke BPEL2oWFN with the following options: |
| 1041 |
|
|
| 1042 |
bpel2owfn -i example.bpel -m petrinet -p communicationonly -f dot -o |
bpel2owfn -i example.bpel -m petrinet -p small -f dot -o |
| 1043 |
|
|
| 1044 |
This command creates a file `example.dot', containing a Graphviz dot |
This command creates a file `example.dot', containing a Graphviz dot |
| 1045 |
representation of the Petri net, and--if the `dot' tool was found in |
representation of the Petri net, and--if the `dot' tool was found in |
| 1065 |
Petri net and the activities of the input BPEL process is not obvious |
Petri net and the activities of the input BPEL process is not obvious |
| 1066 |
for larger processes. To this end, |
for larger processes. To this end, |
| 1067 |
|
|
| 1068 |
bpel2owfn -i example.bpel -m petrinet -p communicationonly -f info |
bpel2owfn -i example.bpel -m petrinet -p small -f info |
| 1069 |
|
|
| 1070 |
displays an information file, consisting of all the Petri net nodes' |
displays an information file, consisting of all the Petri net nodes' |
| 1071 |
roles. |
roles. |
| 1114 |
model to an output file to process it by analysis tools. In this case, |
model to an output file to process it by analysis tools. In this case, |
| 1115 |
we want to create a Fiona open workflow net executing |
we want to create a Fiona open workflow net executing |
| 1116 |
|
|
| 1117 |
bpel2owfn -i example.bpel -m petrinet -p communicationonly -f ownf -o |
bpel2owfn -i example.bpel -m petrinet -p small -f owfn -o |
| 1118 |
|
|
| 1119 |
which creates a file `example.owfn': |
which creates a file `example.owfn': |
| 1120 |
|
|
| 1122 |
{ |
{ |
| 1123 |
generated by: BPEL2oWFN 2.0.1 |
generated by: BPEL2oWFN 2.0.1 |
| 1124 |
input file: `example.bpel' (process `exampleprocess') |
input file: `example.bpel' (process `exampleprocess') |
| 1125 |
invocation: `bpel2owfn -i example.bpel -m petrinet -p communicationonly -f owfn' |
invocation: `bpel2owfn -i example.bpel -m petrinet -p small -f owfn' |
| 1126 |
net size: |P|=5, |P_in|= 1, |P_out|= 1, |T|=2, |F|=6 |
net size: |P|=5, |P_in|= 1, |P_out|= 1, |T|=2, |F|=6 |
| 1127 |
} |
} |
| 1128 |
|
|