Efficient Controllability Analysis of Open Nets

Daniela Weinberg. Efficient Controllability Analysis of Open Nets In Roberto Bruni and Karsten Wolf, editors, Web Services and Formal Methods, Fifth International Workshop, WS-FM 2008, Milan, Italy, September 4-5, 2008, Proceedings, Lecture Notes in Computer Science. Springer-Verlag, September 2008.

Authors

  • paper by Daniela Weinberg 1)

Abstract

A service is designed to interact with other services. If the service interaction is stateful and asynchronous, the interaction protocol can become quite complex. A service may be able to interact with a lot of possible partner services, one partner or no partner at all. Having no partner surely is not intended by the designer. But the stateful interaction between services can be formalized and thus analyzed at design time.

We present a formalization which is centered around a graph data structure that we call interaction graph, which represents feasible runs of a partner service according to the interaction protocol. As interaction graphs suffer from state explosion, we introduce a set of suitable reduction rules to alleviate the complexity of our approach. As our case studies show we are able to analyze the interaction behavior of a service efficiently.

Key words: Controllability, Business process analysis, Formal models in business process management, Process

verification and validation, Petri nets

Case Study/Experimental Results

The experimental results presented in the paper have been calculated using Fiona and the following commands.

To calculate the complete interaction graph of a service:

fiona -t ig service.owfn

To calculate the reduced interaction graph use the command:

fiona -t ig -r service.owfn

And to calculate the operating guideline use the command:

fiona -t og service.owfn -s allnodes

The service files can be found here examples.

We obtained the following results by applying the commands mentioned above to the example services.

Downloads

The slides of the talk are available here.

Referenced Tools

  • BPEL2oWFN (to translate WS-BPEL processes into open nets)

  • Fiona (to decide controllability of an open net)

BibTeX

@inproceedings{Weinberg_2008_wsfm,

Author = {Daniela Weinberg},

Booktitle = {Web Services and Formal Methods, Fifth International Workshop, WS-FM 2008, Milan, Italy, September 4--5, 2008, Proceedings},

Editor = {Roberto Bruni and Karsten Wolf},

Month = sep,

Publisher = {Springer-Verlag},

Series = {Lecture Notes in Computer Science},

Title = {Efficient Controllability Analysis of Open Nets},

Year = {2008}}

1) Humboldt-Universität zu Berlin, Institut für Informatik, 10099 Berlin, Germany