BPEL2PN

Known Issues

Limitations

The current version of BPEL2PN (V1.0) has the following limitations:

It only supports the BPEL 1.1 specification.

It abstracts from data in the BPEL process, i.e. messages and data are modelled as black tokens. Thus the attention is directed to the control flow. Consequently, all other high-level constructs like transition guards and variables were left out, too. So selecting one of two control paths in the Petri net semantics, solved by the evaluation of data, is modelled by a nondeterministic choice. Therefore the resulting Petri net is a low-level Petri net.

Every activity is limited to one correlation set (except the synchronous invoke that is limited to two correlation sets).

Attribute enableInstanceCompensation is ignored. Therefore it is not possible to compensate a process instance, i.e. the entire BPEL process. This is, however, no real limitation: You only need to redefine the process as a scope and embed this scope in a process. Then, the old process can be compensated.

Error Reports and Problems

BPEL2PN is a prototype of a parser transforming a BPEL process into a Petri net according to the Petri net semantics developed in [Sta05]. It is only a brute-force transformation which is a starting point for further research.

If an error occurs during the transformation of a BPEL process, save the complete error (screen shot of the shell, for instance). Otherwise, if you detect a semantic error in the generated Petri net, describe this error. Please, send all the error information together with your BPEL file to the contact person. I will try to fix the error within one week.

Further Work

The development of BPEL2PN ended. A successor tool, BPEL2oWFN, was released and will be subject of ongoing development. For more information, see the BPEL2oWFN website.

The models generated by the present version of our parser can be seen as brute force models. The generated models are significantly larger than typical manually generated models. This is due to the fact that the Petri net patterns are complete, i.e. applicable in every context. For a particular process, many of the modelled features are unused. For instance, if a basic activity cannot throw any error, many of the error handling mechanisms in the surrounding compound activity can be spared. Furthermore, to decide if a specific property holds, it is often sufficient to restrict the patterns to specific aspects. To prove the correct inter-operation of two BPEL processes, for instance, it is sufficient to restrict the attention to communication aspects of the patterns, while internal actions can be abstracted away.

In ongoing projects, we aim at an improved translation where several Petri net patterns with different degree of abstraction are available for each BPEL activity. Using static analysis on the BPEL code, we want to select the most abstract pattern applicable in a given context. We believe that model sizes can be drastically reduced this way thus alleviating the state explosion problem inherent to model checking.

Our goal is a technology chain that, starting at a BPEL process, performs static analysis. Based on the analyzed information, the translator selects the most abstract pattern for each activity that is feasible in the analyzed context and synthesizes a Petri net model. On the Petri net model, a model checker evaluates relevant properties. The analysis results (e.g., counter example paths) are translated back to the BPEL source code.