Automated Adaptor Generation for Services Based on Pushdown Model Checking

Service adaptation is a promising solution for mismatches in service composition by introducing a mediate service called adaptor to coordinate interactions of services. In a previous work, an approach of non-regular service adaptation using model checking has been proposed for solving behavior mismatches. The approach uses pushdown automata as behavior model of adaptors so that non-regular interactions of services can be captured. Furthermore, adaptation and verification are integrated using model checking and the adaptor can be generated automatically without adaptation contracts being specified. However, though behavior mismatch free is guaranteed in the approach, we found there are usually several or more candidates which satisfy this criteria and may need to be further selected with other requirements. This paper follows the approach and focuses on requirements helpful to automated adaptor generation. Because of the use of pushdown system model, we are especially interested in properties related to unbounded messages, i.e., messages being sent and received arbitrary multiple times, which characterize non-regular behavior in service composition. This paper also shows experimental results from a prototype tool as well as directions for building a BPEL adaptor once behavior of an adaptor is generated by our approach.