PUMA
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. In: IEEE European Conference on Web Services (ECOWS'06) (Zurich, Switzerland, 4-6 December 2006). Proceedings, pp. 287 - 296. A. Bernstein, T. Gschwind, and W. Zimmermann (eds.). IEEE Computer Society, Los Alamitos, CA, 2006.
 
 
Abstract
(English)
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 long-running computations and 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.
URL: http://fmt.isti.cnr.it/~mtbeek/asoap.pdf
Subject Formal methods
Model checking
Web services
Network protocol
SOAP
UMC
C.2.2 Network Protocols. Protocol verification
D.2.4 Software/Program Verification. 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