An Adaptable Formal Model for Web Services Protocols

Agents require standard and reliable protocols to interact with service providers in order to provide high quality customer service over the Web. Many useful Web services protocols are coming on the market, but are often ambiguously specified by protocol designers and not fully verified. This can lead to interoperability problems among implementations of the same protocol as well as high software maintenance costs. We have recently proposed a formal hierarchical automata-based framework that aims to address these issues. In this paper, we extend our framework to overcome the two identified limitations, re-usability and adaptability, and describe how they are useful for conformance checking and for our observer-based technique for property specification. We also apply the extended framework on the WS-business activity´s atomicoutcome protocol suite and discuss our experience using the model.