Analyzing Mediated Service Protocol Interactions Considering User's Expectation

A main promise of the service-oriented computing paradigm is to support a seamless interaction between service protocols. Given the inherent autonomy, heterogeneity, and continuous evolution of Web services, mismatches usually exist between service protocols. Hence, to efficiently identify and then select a suitable service protocol among functionally equivalent candidate service providers to achieve a certain business goal, an important criterion to the requestor is the knowledge about whether or not, and under which conditions, expected service interactions can be mediated. In this paper we propose a formal technique to verify whether an expected service interaction is adaptable. We first present our observation that a mediated service interaction is synchronizable. Then, we formally model a protocol scenario (i.e., a part of a service protocol that can be enacted in an expected interaction) and an adapter, generate an adaptation logic, and formalize a mediated service interaction and its conversation. These enable one to perform a formal verification which examines whether or not, as well as under which condition, an expected interaction is achievable. The technique presented in this paper complements the efforts of adapter synthesization for ensuring the achievability of a certain expected interaction.