Research on service composition based on bounded model checking
Zhang Li · Computer Engineering and Applications Journal · 2012
Large-scale automatic service composition is the main problem in Web Service technology. The classic means of service composition have little flexibility and are applied in small-scale services. Based on service descrip-tion by using finite state machine, a way of bounded model checking techniques applied in modeling large-scale ser- vice composition is proposed, in which user requirements are translated into linear temporal logic formulas and the technology of solving satisfiability problem is used to discover the limited length composed solutions of services quickly.Experimental results show that it is feasiable to apply the techniques of bounded model checking to look for the solution of large-scale service composition.