Model-Based Simulation of SOAP Web Services from Temporal Logic Specifications

摘要

This paper presents a methodology for generating a web service "stub" that simulates the behaviour of a real-world SOAP web service. The simulation is driven by a formal description of the original service's input and output parameters, messages, and ordering constraints between messages, using an extension of Linear Temporal Logic called LTL-FO+. This logic is rich enough to express complex behaviours taken from real-world web services, where the structure of future messages and valid parameter values are interdependent. Given a history of previous interactions, a sound, symbolic algorithm is described that generates on-the-fly a new message that is a valid continuation of that history with respect to the LTLFO + specification. By providing a faithful placeholder for an actual third-party web service, this algorithm can be used as a development and testing tool. Empirical evaluation shows how such an approach outperforms a previous attempt that relied on a model checker to produce each new message.