Adaptive service composition based on runtime verification of formal properties

Service-Oriented Computing (SOC) has been used in business environments in order to integrate heterogeneous systems. The dynamic nature of these environments causes changes in the application requirements. As a result, service composition must be flexible, dynamic and adaptive, which motivate the need to ensure the service composition behavior at runtime. The development of adaptive service compositions is still an opportunity due to the complexity of dealing with adaptation issues, for example, how to provide runtime verification and automatic adaptation. Formal description techniques can be used to detect runtime undesirable behaviors that help in adaptation process. However, formal techniques have been used only at design-time. In this paper, we propose an adaptive service composition approach based on the lightweight use of formal methods. The aim is detecting undesirable behaviors in the execution trace. Once an undesirable behavior is detected during the execution of a service composition, our approach triggers an adequate reconfiguration plan for the problem at runtime. In order to evaluate the effectiveness of the proposal, we illustrate it with a running example.