Formal verification of mediatedweb service interactions considering client´s expected behaviours

This paper proposes a formal technique to verify whether or not an expected interaction is adaptable. We first present our observation that a mediated service interaction is synchronizable. This fact is a prerequisite of our approach. Hereafter, we formally model a protocol scenario (i.e., a part of a service protocol to be enacted in an expected interaction) and an adapter, generate an adaptation logic, and formalize a mediated service interaction and its conversation. These formalization enables one to perform a formal verification that checks 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.