We study fundamental problems related to the behavior of stateful services. We identified several specific challenges related to the interference between control flow and communication. We adopt a rigorous approach based on formal models such as finite state machines and Petri nets. These models are linked to reality through translations from industrial languages such as WS-BPEL. In some cases, we are also able to directly lift results to WS-BPEL itself.
On the level of formal models, we are able to apply state-of-the-art techniques for the verification of services and service collaborations. As services are essentially open systems, a fundamental kind of reasoning concerns the existence of a correctly interacting partner. Going one step further, we are able to compute a finite characterization of the (typically infinite) set of all correctly interacting partners for a given service. We have turned these results into efficient tools.
We could show that several interesting problems for services can be traced down to these fundamental questions on partners. Examples are the synthesis of a behavioral adapter between incompatible services, the selection of useful test cases, support for service instance migration, or the study of service substitution as needed in contract scenarios.
- Wolfgang Reisig, Karsten Wolf, Jan Bretschneider, Kathrin Kaschner, Niels Lohmann, Peter Massuthe, and Christian Stahl. Challenges in a Service-Oriented World
- Niels Lohmann. A Feature-Complete Petri Net Semantics for WS-BPEL 2.0
- Dieter König, Niels Lohmann, Simon Moser, Christian Stahl, and Karsten Wolf. Extending the Compatibility Notion for Abstract WS-BPEL Processes
- Niels Lohmann, Peter Massuthe, Christian Stahl, and Daniela Weinberg. Analyzing Interacting WS-BPEL Processes Using Flexible Model Generation
- Karsten Wolf. Does my service have partners?
- Niels Lohmann, Peter Massuthe, and Karsten Wolf. Operating Guidelines for Finite-State Services
- Niels Lohmann and Daniela Weinberg. Wendy: A tool to synthesize partners for services
- Christian Gierds, Arjan J. Mooij, and Karsten Wolf. Reducing adapter synthesis to controller synthesis
- Kathrin Kaschner. Conformance testing for asynchronously communicating services
- Nannette Liske, Niels Lohmann, Christian Stahl, and Karsten Wolf. Another Approach to Service Instance Migration
- Wil M. P. van der Aalst, Niels Lohmann, Peter Massuthe, Christian Stahl, and Karsten Wolf. Multiparty Contracts: Agreeing and Implementing Interorganizational Processes
- Niels Lohmann and Karsten Wolf. Realizability is controllability
- Niels Lohmann and Karsten Wolf. Artifact-Centric Choreographies