A formal framework for service mashups with dynamic service selection

The service mashup programming paradigm is a blooming faction of service oriented Architecture for developing web applications. A mashup application constructs its functionality by combining data, presentation and functionalities obtained from online services published by service providers such as Google and Amazon. This paradigm significantly facilitates the implementation of application and reduces the workload. But it also makes the application rely on the availability and qualities of the online services which beyond its control in which case the robustness of the system requires more concern. This paper proposes a formal model to specify and analyze the behavior and robustness of service mashups under a certain environment where some services may become unavailable. The specification contains both system specification and environment situation. Refinement theory are employed to specify the correctness of dynamic service selection. The framework realizes the service selection by allowing virtual service requests to be handled by any online service having consistent interface and refined functionality. The framework provides a clear definition of the robustness of mashup systems and proposes several rules as well as approaches to preserve the robustness during the development and maintenance of the system.