Istituto di Scienza e Tecnologie dell'Informazione     
Ter Beek M. H., Gnesi S., Mazzanti F., Moiso C. Formal Modelling and Verification of an Asynchronous Extension of SOAP. The document has been submitted to Conference: 26th IFIP WG 6.1 International Conference on Formal Methods for Networked and Distributed Systems (FORTE'06), Paris, France, 26-29 September 2006, Technical report, 2006.
Current web services are largely based on a synchronous request-response model that uses the Simple Object Access Protocol SOAP. Next-generation telecommunication networks, on the contrary, are characterised by the need to handle asynchronous interactions among distributed service components, e.g. to deal with events produced by the network resources. As these worlds are more and more converging into a single application context, several solutions have been proposed to deal with asynchronous events in the context of web services. In this paper we formalise and verify one such approach, viz. an original asynchronous extension of SOAP, and draw some conclusions. The formal model is specified as a set of communicating state machines. The semantics of the model is seen as a doubly-labelled transition system, and its behavioural properties are expressed in the action- and state-based temporal logic mu-UCTL and verified with the on-the-fly model checker UMC.
Subject Web services, SOAP protocol, UMC model checker
D.2.4 Software/Program Verification . Formal Methods, Model Checking

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional