Research Article
Formal verification of mediated web service interactions considering client's expected behaviours
@INPROCEEDINGS{10.4108/ICST.COLLABORATECOM2009.8270 , author={Zhangbing Zhou and Sami Bhiri and Lei Shu and Manfred Hauswirth}, title={Formal verification of mediated web service interactions considering client's expected behaviours}, proceedings={5th International ICST Conference on Collaborative Computing: Networking, Applications, Worksharing}, proceedings_a={COLLABORATECOM}, year={2009}, month={12}, keywords={Formal verification Logic Privacy Protocols Switches System recovery Web services}, doi={10.4108/ICST.COLLABORATECOM2009.8270 } }- Zhangbing Zhou
Sami Bhiri
Lei Shu
Manfred Hauswirth
Year: 2009
Formal verification of mediated web service interactions considering client's expected behaviours
COLLABORATECOM
ICST
DOI: 10.4108/ICST.COLLABORATECOM2009.8270
Abstract
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.
