/[bpel2owfn]/bpel2owfn/manual/2.0.x/bpel2owfn.txt
ViewVC logotype

Diff of /bpel2owfn/manual/2.0.x/bpel2owfn.txt

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 1.3 by nielslohmann, Fri May 11 15:29:16 2007 UTC revision 1.4 by nielslohmann, Fri Jun 15 15:48:30 2007 UTC
# Line 3  GNU BPEL2oWFN Line 3  GNU BPEL2oWFN
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
# Line 67  This oWFN can be used to: Line 67  This oWFN can be used to:
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
# Line 117  Output Petri Net      The generated Petr Line 122  Output Petri Net      The generated Petr
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
# Line 143  BPEL2oWFN supports the following command Line 149  BPEL2oWFN supports the following command
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'
# Line 201  BPEL2oWFN supports the following command Line 218  BPEL2oWFN supports the following command
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    
# Line 258  When invoking BPEL2oWFN several modes ar Line 275  When invoking BPEL2oWFN several modes ar
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
# Line 294  These options control some Petri net-rel Line 315  These options control some Petri net-rel
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
# Line 351  supported. There are invoked by the foll Line 372  supported. There are invoked by the foll
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
# Line 391  supported. There are invoked by the foll Line 412  supported. There are invoked by the foll
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    
# Line 462  supported. There are invoked by the foll Line 483  supported. There are invoked by the foll
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
# Line 483  In this section we show some examples ho Line 504  In this section we show some examples ho
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  *****************************  *****************************
# Line 815  Code Type          Description Line 843  Code Type          Description
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.
# Line 870  Code Type          Description Line 898  Code Type          Description
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    
# Line 996  standard values of several attributes (e Line 1027  standard values of several attributes (e
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    
# Line 1008  The generated Petri net model consists o Line 1039  The generated Petri net model consists o
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
# Line 1034  modeled semantics. Especially the correl Line 1065  modeled semantics. Especially the correl
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.
# Line 1083  the intended behavior of the BPEL proces Line 1114  the intended behavior of the BPEL proces
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    
# Line 1091  which creates a file `example.owfn': Line 1122  which creates a file `example.owfn':
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    

Legend:
Removed from v.1.3  
changed lines
  Added in v.1.4

savannah-hackers-public@gnu.org
ViewVC Help
Powered by ViewVC 1.1.26