A Model Checking Approach to Analyzing Timed Compatibility in Mediation-Aided Composition of Web Services

Recently, the mediation-aided approach is attracting more attention in Web service composition, in the meanwhile, temporal constraints are regarded as an important aspect to ensure the correctness and QoS in service compositions. This combination leads to a new challenge in analyzing the timed compatibility of mediation-aided service composition. Unfortunately, existing model checking based approaches are lack of the ability of transform mediation-aided service composition to Time Automata (TA) models, and suffer from state space explosion for large-scale and complex compositions. In this paper, we present a new model checking approach to analyzing timed compatibility. Firstly, mediation-aided service composition is automatically decomposed into fragments. Secondly, each fragment is transformed into a TA. Finally, the temporal constraints are checked by the queries of observing TAs. Compared with existing approaches, our approach is able to check timed compatibility of mediation-aided service composition, and is more efficient than them.