关键词: 限界模型检查，Web服务，行为失配检测，可满足性模理论

Abstract: Due to inconsistent of the interface type or interaction protocol, services can not be combined in the right way. Web services mismatch detection can accurately capture the mismatch points,which creates a foundation for rcalizing right interaction, avoid invalid composition. This paper presented a method for detecting mismatch of Web services based on Satisfiability Modulo Theories(SM7).The issue of detecting mismatch of Web services can be transformed into the problem of existence model checking that 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 that the logic formula is satisfiable or not. Finally, an example was given to explain the process of Web service mismatch detection.

Key words: Bounded model checking, Web service, Behavioral mismatch detection, Satisfiability modulo theories