Web service composition based on bounded model checking

With the acceptance of service-oriented architecture (SOA) in many application domains and rapidly growing number of available services, it is now a challenge to effectively compose services to meet users´ needs. In this paper, we present a service composition method based on bounded model checking technique. Specifically, a web service community includes a set of web services whose behavior are specified as labeled transition system and composition requirements are described by linear temporal logic formulas, then bounded model checking tools can be used to automatically synthesize composite services that use only the services in the service community to realize composition requirements. Experiment results show that this method can adapt to large-scale web service composition scenarios.