 Introduction

Correctness plays an important role in service-oriented systems, as they in creasingly realize business processes or other important infrastructures. Because failures of a single service may affect all other participants of the composition, thorough testing or verification is of paramount importance. In previous work [], we argued that partner synthesis is not only an effective means to check the correctness of single services, but can also be used to synthesize communication skeletons, construct operating guidelines, generate test suites, realize interac tion models, correct choreographies, configure business processes, or synthesize adapters. Further references can be found in a survey []. Thereby, a part ner of a service is another service such that their composition is correct (e. g., deadlock-free, sound, or weakly terminating).

Conceptually, a partner is synthesized by first overapproximating the service's behavior in any possible composition and then removing undesired states yielding deadlocks or livelocks. Unfortunately, the complexity of the partner synthesis is exponential in the size of the service; that is, both in the number of states and the size of the interface. Even worse, the service's behavior itself can already suffer from the state space explosion problem [], which makes the overall complexity of partner synthesis devastating.

As partner synthesis focuses on the external behavior of a service (i. e., its communication protocol), the internal behavior is only important when internal decisions are modeled. To this end, this paper aims at reducing internal behavior of a service while preserving its external behavior. As a result, we can construct partner services with reduced effort. We therefore sketch partner synthesis in the next section. As one contribution, we also survey in Sect.  different approaches to leverage the complexity to classify our reduction. Section  provides the main contribution of this paper: We adjusted several state space reduction rules to reduce internal service behavior. To assess our approach, we implemented it and discuss in Sect.  some first experimental results and the impact of the reduction to the partner synthesis, before Sect.  concludes the paper.

 Partner synthesis in a nutshell

We shall briefly sketch the partner synthesis approach of Wolf []. Given a service model, a partner cannot observe the service's state at runtime. Hence, the only information a partner can rely on are () the service model and its behavior (i. e., its state space), () its own actions from the past, and () the asynchronous messages it receives from the service or synchronizations with the service.

Consequently, a partner can only make a vague statement on the concrete state of a service, and can only guess a set of states (called knowledge) the service might be in. For instance, the initial knowledge of a partner consists of all states of the service it can reach without influence of the partner; that is, all states the service can reach by performing internal transitions (also called silent or τ -transitions) or by sending asynchronous messages to the partner. Each action of the partner results in changed knowledge. For instance, sending a message to the service may result in additionally enabled receiving transitions. After building all possible knowledges and removing "bad" knowledges; that is, knowledges which imply unwanted behavior of the composition (such as deadlocks or livelocks), the remaining graph (unless empty) can be used as a partner. The partner synthesis algorithm is implemented in two tools, Fiona [] and Wendy [], we shall discuss later.

 Reduction techniques for partner synthesis

There are several aspects that yield in the high complexity of the partner synthesis approach. For some of theses aspects already exist approaches to leverage the associated complexity.

State space. On source of complexity is the size of the state space of the service. Each knowledge is a subset of the service's states. Since services often employ concurrency, already this state space may be exponentially in the size of the service model. This state explosion can be fought in different fashions, and these state space reduction approaches can be classified as follows.

One idea is to reduce the original model (e. g., the Petri net or WS-BPEL process) before the calculation of the state space. The most prominent example for such an a priori reduction are Petri net reduction rules []. Applied to service models, these rules already allow to remove some internal behavior. However, experiments with business process models [] show that their effect does not hardly justifies the required calculation time.

Another idea is not to generate the complete state space, but only a smaller fragment of it. An example for such an on-the-fly reduction are partial order tech niques, for instance CTL * preserving partial order reduction []. First experiments with such a technique implemented in the tool Fiona are promising.

Finally, state space reduction techniques can also be applied a posteriori ; that is, after the full state space is built, but before the partner synthesis. Such reduction rules [] were already employed to reduce a characterization of all livelock-freely interaction partners [], but not for the partner synthesis itself. This shall be the contribution of this paper.

Knowledge. Once the state space is built, the number of knowledges is another source of complexity. Here, we face two problems. First, a lot of "bad" knowledges are generated, but later removed because they contain unwanted behavior. For instance, a service model may contain a deadlock which is only reached after following a certain communication protocol. To avoid such unnecessary calculation, static analysis techniques can be used to preprocess the state space and to avoiding the calculation of "bad" knowledges as early as possible [].

Second, not all knowledges need to be calculated in case only the existence of a partner is relevant. Such a (possibly less permissive) partner is usually much smaller. Weinberg [] presents several partner reduction rules which turn out to be very effective during the partner synthesis of industrial service models [].

Representation. Finally, symbolic data structures such as binary decision dia grams [] may help to represent the state space and the knowledges in a compact manner. Early experiments [] show that this technique known from model checking is also very effective when applied during partner synthesis.

The presented reduction techniques are modular, although they cannot be arbitrarily mixed. For instance, the tool Fiona [] generates the state space on the fly and implements partial order reduction techniques, partner reduction rules, and symbolic representation. A reimplementation of Fiona, Wendy [], generates the complete state space a priori to perform static analysis to avoid the calculation of "bad" knowledges. It also implements partner reduction rules. A case study [] demonstrates that Wendy clearly outperforms Fiona. As Wendy does not implement any state space reductions, we shall focus on this aspect in the remainder of the paper.

 Reduction of internal behavior

As mentioned earlier, Petri net reduction techniques are not effective enough to fight the state space reduction. Furthermore, on-the-fly reduction techniques cannot be combined with the powerful preprocessing techniques that avoid the generation of "bad" knowledge. Consequently, we shall investigate how a posteriori reduction techniques can be combined with partner synthesis.

To reduce the complexity of partner synthesis, we follow one idea: States of the service, that would always appear in the same knowledge, should be merged before the actual partner synthesis. As sketched in Sect. , this reduction particularly affects internal transitions, because -by definition -knowledge consists of those states that can be reached without interaction with the partner. Our approach takes the state space of a service model as input and constructs a reduced state space such that both the original and the reduced state space yield the same generated partner.

To achieve this goal, we employed state space reduction rules from Juan et al. []. These rules were defined to preserve IOT failure equivalence [], which is very closely related to the preservation of external behavior we are interested in. Figure  depicts four of these rules. Thereby, a dashed arc stands for an arbitrary number of transitions with an arbitrary label. The rules are defined on the behavior of a service model and may appear very technical when considered in isolation. Nevertheless, the first two rules may allow the application of other rules. As special case of the third rule is when s 1 has no outgoing transitions other than the internal transition, see Fig. (d). Only this restricted setting is covered by a Petri net reduction rule []. In general, state space reduction rules allow for more reduction, because they can be applied on a simpler model and do not need to take concurrency into account. Juan et al. [] present more rules, but we refrain from a discussion of all of them. For instance, several rules deal with initial states. Furthermore, no original rule was aware of final states which are important in the area of services to distinguish desired final states from deadlocks or to detect livelocks.

Redundant parallel transitions

 Experimental results: effect to partner synthesis

We implemented the reduction rules described in the prior section as a component of Wendy []. It takes a Petri net service model as input, calls LoLA [] to generate a state space and then iteratively applies the reduction rules until a fixed point is reached; that is, no more rules can be applied. The output is a reduced state space which is then used during the partner synthesis. The integration of the reduction component is still in an early stage of development.

As a proof of concept, we analyzed several WS-BPEL services from a con sulting company. Each process consists of around  WS-BPEL activities and models communication protocols and business processes of different industrial sectors. We translated the WS-BPEL processes into Petri nets using the compiler BPEL2oWFN implementing a feature-complete Petri net semantics []. Further more, the "Philosophers" service is an academic example.

Table  summarizes the results regarding the reduction: For most industrial models, nearly all internal transitions could be removed and the state space could be reduced dramatically. This is particularly important, because knowledges consist of subsets of these state spaces, so even a small reduction may have an exponential effect. The SMTP protocol shows, however, that the reduction is The partly devastating can be explained by the prototypic status of the implementation. Nevertheless, the runtime of the reduction can be seen as a worthwhile investment, as shown by Table . We see that the synthesis times are usually much faster when the reduction is applied. Of course, we also need to take the reduction time into account. Nevertheless, only when analyzing the "Philosopher" model, the additional time does not pay off. Experiences from the implementation of Petri net reduction rules (i. e., parallel execution or index structures) may help to decrease the runtime by an order of magnitude.

More importantly, we can observe a dramatical reduction of around  % in the consumed memory. This allows us to synthesize partners for service models using a few megabytes rather than gigabytes.

 Conclusion

Summary. In this paper, we discussed several sources of complexity of partner synthesis. We identified a large state space and in particular internal transitions as one reason partner synthesis might be intractable for larger service models. To tackle this problem, we presented a reduction technique that aims at reducing the internal behavior of service models. This technique is modular; that is, can be integrated in existing partner synthesis approaches. A prototypic integration into the partner synthesis tool Wendy [] demonstrated principal effectiveness of the reduction. We observed a dramatic decrease in memory consumption which allowed us to apply partner synthesis to models we could not analyze before. This reduced memory reduction, however, is currently traded by a suboptimal runtime of the reduction.

The approach has another advantage: it is compositional. Suppose the state space of the net is too large to be calculated. As this calculation is a prerequisite for the synthesis algorithm, no partner could be computed. The rules, however, allow for a compositional approach. That is, we can () divide the net into parts, () apply the reduction rules to the state space of each part, and () compose  We currently face a software bug when analyzing the reduced SMTP protocol model. reduced state spaces. The interested reader is referred to [] for a detailed discussion.

Lessons learnt. In retrospective, the results of this paper seem obvious and the approach straightforward. However, two questions were open in the run-up of this paper: First, little experimental results were published on the practical applicability of the reduction rules from Juan et al. [] and their effectiveness to real-life service models. Second, the exact effect of the reduction to partner synthesis was unclear. In particular, we did not foresee that reduced internal behavior could have such a positive effect on the memory consumption. Also the fact that already four reduction rules have such an effect was unclear. The "Philosophers" model further showed that much fewer knowledges need to be calculated when synthesizing partners.

We would like to point out that only a prototypic implementation and access to realistic service models allowed us to perform experiments and to answer these questions. Thereby, the modular architecture of the partner synthesis tool Wendy facilitated the integration of the reduction rules to the partner synthesis. These experiences follow the observations we described in a recent survey []. Both the tool Wendy [] and the experimental results are available via the Web site http://service-technology.org/live [].

Future work. In future work, several open issues need to be approached. As already pointed out, we need to improve the efficiency of the rule application. From a conceptual point of view, a combination of the presented approach and partial order reduction techniques would be promising. Partial order reduction aims at avoiding the state space explosion by not enumerating all possible orders of transitions and intermediate states. This usually results in very small and also simpler structured state spaces. This in turn should boost the applicability of the reduction rules. Finally, a look at related rules [] may allow for further reduction.