Towards a Formalization of Contracts for Service Substitution

In a service-oriented system, service substitution can be used to repair faults, improve performance, and/or enhance resilience via graceful degradation. Correct service substitution must preserve the essential properties of the system, particularly the proper termination and/or liveness. However, ensuring correct service substitution poses some challenges. The main obstacle is that, in the general case, the behavior of services is opaque to service designers due to the autonomy of services. While the bulk of prior researches on service substitution assume that services advertise their interaction protocols (e.g., in the form of BPEL), existing services (i.e., in the form of WSDL) rarely do so. In this paper, we study the problem of service substitution under the assumption that services do not expose their interaction protocols. To this end, we characterize the behavior of interacting services by means of contracts consisting purely of input/output messages and message exchange patterns revealed in WSDL interfaces. On the other hand, the behavior of service compositions is assumed to be known to service designers. In this setting, we define notions of compatibility for self-contained systems and for open systems. Based on these notions, we propose a theory of contracts for service substitution. We also study a notion of degraded substitution based on the "may-", "should-" and "must-" testing pre-orders.