The Community for Technology Leaders
Green Image
Issue No. 02 - Second (2012 vol. 5)
ISSN: 1939-1374
pp: 192-206
Sylvain Hallé , Université du Québec à Chicoutimi, Chicoutimi
Roger Villemaire , Université du Québec à Chicoutimi, Chicoutimi
An increasing number of popular SOAP web services exhibit a stateful behavior, where a successful interaction is determined as much by the correct format of messages as by the sequence in which they are exchanged with a client. The set of such constraints forms a "message contract” that needs to be enforced on both sides of the transaction; it often includes constraints referring to actual data elements inside messages. We present an algorithm for the runtime monitoring of such message contracts with data parameterization. Their properties are expressed in {\rm LTL}\hbox{-}{\rm FO}^+, an extension of Linear Temporal Logic that allows first-order quantification over the data inside a trace of XML messages. An implementation of this algorithm can transparently enforce an {\rm LTL}\hbox{-}{\rm FO}^+ specification using a small and invisible Java applet. Violations of the specification are reported on-the-fly and prevent erroneous or out-of-sequence XML messages from being exchanged. Experiments on commercial web services from and Google indicate that {\rm LTL}\hbox{-}{\rm FO}^+ is an appropriate language for expressing their message contracts, and that its processing overhead on sample traces is acceptable both for client-side and server-side enforcement architectures.
Web services, runtime monitoring, temporal logic.
Sylvain Hallé, Roger Villemaire, "Runtime Enforcement of Web Service Message Contracts with Data", IEEE Transactions on Services Computing, vol. 5, no. , pp. 192-206, Second 2012, doi:10.1109/TSC.2011.10
99 ms
(Ver )