start reading here

Story view

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.

Our techniques may also be applied beyond the study of actual services, for instance for reasoning about service choreographies or interaction between artifact-centric business processes.

List view