5th International ICST Conference on Collaborative Computing: Networking, Applications, Worksharing

Research Article

Formal verification of mediated web service interactions considering client's expected behaviours

Download625 downloads
  • @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
Zhangbing Zhou1,*, Sami Bhiri1,*, Lei Shu1,*, Manfred Hauswirth1,*
  • 1: Digital Enterprise Research Institute, National University of Ireland, Galway
*Contact email: zhangbing.zhou@deri.org, sami.bhiri@deri.org, lei.shu@deri.org, manfred.hauswirth@deri.org

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.