A method for detecting mismatch of time-aware Web services based on SMT

Considering the timed properties between the interactions of Web services, we model the Web services with timed properties formally and propose a method for detecting mismatch of time-aware Web services based on Satisfiability Modulo Theories (SMT) in this paper. The issue of detecting mismatch of Web services can be transformed into the problem of existence model checking whether a deadlock is reachable or not between the interaction of the services, and the issue of existence model checking can be transformed into the problem whether the logic formula is satisfiable or not.