ASEHA: A Framework for Modelling and Verification ofWeb Services Protocols

Agents require standard and reliable protocols to interact with different service providers in order to provide high quality service to customers over the Web. Many useful protocols are coming into the market, but are often ambiguously specified by protocol designers and not fully verified. These can lead to interoperability problems among implementations of the same protocol and high software maintenance costs. In this paper, we propose a hierarchical automata-based framework to model the necessary features of protocols to verify their correctness. Our experience shows that the graphical models help uncover subtle scenarios and reduce, if not eliminate, ambiguities. We illustrate our formalism with a version of WS-atomic transaction protocol