Checking Composition-Aware Service Substitutability

In many applications involving composite Web services, one or more component services may become unavailable, or no longer satisfy the quality requirements. This leads to the problem of identifying other components that can substitute the faulty component, while maintaining the overall functionality of the composite service. Given a candidate service that offers the desired functionality, it is often necessary to select the most preferred substitution based on the correctness of the global behavior of the composite service. Such a candidate is selected from a repository of public representations of possible components where internal and private behavior are hidden. In this paper, we present and implement an approach to determine whether a possible candidate can substitute a part of a composite service while preserving the deadlock freeness property. At the same time, we propose a behavioral abstraction of web services, namely the symbolic observation graph, that preserves their privacy while allowing the modular verification of their correction. The approach is illustrated on a realistic use case involving three services (a provider, a distributor and a client).