Petri Nets 2010, ACSD 2010 - Braga, Portugal


ACSD 2010

Braga, Portugal, June 21-25, 2010
Petri Nets 2010, ACSD 2010 - Braga, Portugal

Tutorials | TT2: Analysis and Synthesis of (Web) Service Behavior

Authors: Karsten Wolf1, Kathrin Kaschner1, Niels Lohmann12, and Christian Stahl2
1Universität Rostock, Institut für Informatik, Rostock, Germany,,
2Technische Universiteit Eindhoven, Department of Mathematics and Computer Science, Eindhoven, The Netherlands,,

Abstract: Web services are made for loose coupling, i.e. composition. Besides semantics (what do exchanged messages mean?) and non-functional properties (how is message exchange realized?), behavior (in which order are messages exchanged?) is a key aspect for achieving a correct composition.
We introduce to formal modeling of service behavior using Petri nets and link formal models to industrial languages. Then we explain a few basic techniques for analyzing and synthesizing service behavior. Subsequently, we demonstrate the applicability of these techniques in a wide range of practically relevant problem settings. The tutorial shall include several tool demonstrations on real service models.

Objective: Petri nets are quite well appreciated as a suitable formal tool in the Web service domain. In the tutorial, we want to present a reasonably small set of basic techniques that is useful in solving a broad range of problems related to services. The material presented in the tutorial covers relevant industrial languages, theoretical modeling and reasoning, and tool support. We will also mention some open problems.

More Information on Content: The web site is closely related to the content of this tutorial.

Tutorial Outline:

  1. Opening and Introduction
    • Motivation, introduction to SOA, SOC, inter-organizational business processes
    • Preview and outline of the tutorial
    • Formal models: open nets, communication, ports, composition
    • Basic notions for services: partner, correctness
    • Tool demo
  2. Industrial Service Descriptions
    • Formal semantics for industrial languages: WS-BPEL, UML, YAWL, BPMN
    • Translation of services, choreographies, and service collaborations into Petri nets
    • Translation of formal models into WS-BPEL and BPMN
    • Tool demo
  3. Fundamental Algorithms for Service Behavior
    • Compatibility (analysis of behavior): definition, state space verification, reduction techniques, case study: BPEL4Chor
    • Controllability (synthesis of behavior): definition, partner synthesis in different settings, reduction techniques
    • Characterization of behavior: definition, construction of operating guidelines
    • Tool demo
  4. Applications that Support Service Providers in the SOA Triangle
    • Sanity checks (soundness, controllability) and diagnosis
    • Test case generation
    • Public view generation
    • Substitutability, accordance, transformation rules
    • Instance migration/runtime substitutability
    • Tool demo
  5. Applications that Support Service Brokers in the SOA Triangle
    • Adapter synthesis, semantic constraints
    • Service discovery, behavioral constraints
    • Tool demo
  6. Applications Outside the SOA Triangle
    • Contract based composition
    • Correction assistance for incorrect choreographies
    • Tool demos: Rachel
  7. Conclusion and Discussion

Speaker's biography:
Karsten Wolf is a full professor at the University of Rostock. He is co-author of about 30 reviewed papers on service behavior. He also developed the verification tool LoLA that is suitable for verifying service behavior. Karsten has been a co-chair of the PC for the workshop Web Services and Formal Methods 2008 and the 30th Int. Conference on Petri Nets and Other Models of Concurrency 2009. He will be a co-chair of the PC for the Int. Conf. Business Process Management 2011. He served many times in PCs of Petri net related conferences and workshops. He is chair of the GI working group Petri nets and related system models. He is one of the initiators of the regional workshops ZEUS (Central European Workshop on Web Services and their Composition).

Kathrin Kaschner is a PhD student in Karsten's group and co-author of 5 re- viewed publications on service behavior. In her PhD project, she is concerned with service characterization and applications including service discovery, test case generation, and fundamental algorithms for services. She has been involved in the development of tools related to the analysis and synthesis of service be- havior.

Niels Lohmann is a PhD student in Karsten's group and co-author of about 30 reviewed publications on service behavior. In his PhD project, he investigates diagnosis and correction of services and choreographies and develops the tool Rachel. He is also working on formal semantics of industrial service speci ca- tion languages. He has developed several tools for analysing and synthesizing services and coordinated the whole service related tool development in the Ros- tock group. He is one of the initiators of the regional workshops ZEUS (Central European Workshop on Web Services and their Composition).

Christian Stahl is a Postdoc at TU Eindhoven. He is co-author of about 20 reviewed publications on service behavior. His research is focussed on behavioral service substitution. He has also been working on a Petri net semantics for the industrial language WS-BPEL.