Web Services, European Conference on (2006)
Dec. 4, 2006 to Dec. 6, 2006
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ECOWS.2006.22
Maurice H. ter Beek , ISTI--CNR, Italy
Stefania Gnesi , ISTI--CNR, Italy
Franco Mazzanti , ISTI--CNR, Italy
Corrado Moiso , Telecom Italia, Italy
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 actionand state-based temporal logic \mu-UCTL and verified with the on-the-fly model checker UMC.
S. Gnesi, F. Mazzanti, M. H. Beek and C. Moiso, "Formal Modelling and Verification of an Asynchronous Extension of SOAP," 2006 4th IEEE European Conference on Web Services(ECOWS), Zurich, 2006, pp. 287-296.