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.