Model checking of timed compatibility for mediation-aided web service composition: A three stage approach

Currently, modeling and analyzing timed compatibility of Petri net based mediation-aided Web service composition by model checking are attracting increasing attention in the expert and intelligent systems community. However, existing methods cannot handle mediation-aided Web service composition involving complex mediation transitions, suffer from low efficiency owing to the larger size of time automata (TA) models, or are unable to automatically check temporal constraints whose activities do not include exchanged messages by observing TA. In this paper, we present a novel three-stage approach for analyzing timed compatibility of mediation-aided Web service composition via model checking. First, stage 1 treats each service in Petri net based mediation-aided Web service composition as a fragment. Second, stage 2 transforms fragments into a time automata net (TAN) based on structure transformation and interactive message transformation. Finally, stage 3 checks all types of temporal constraints. The main impact of our approach on expert and intelligent systems involves the following aspects: 1) mediation-aided service composition with complex mediation transitions can be dealt with; 2) compact TAN can be constructed for fragments in which the number of states and arcs is dramatically decreased and the verification time is extremely reduced compared with existing methods; and 3) temporal constraints whose activities have or do not have exchanged messages can be located in TAN. The main significance of our approach in the field of expert and intelligent systems is that it can greatly reduce the risk of making business decisions and the cost of handling temporal violations, and improves the innovation capability of enterprises.