Automated Adaptor Generation for Behavioral Mismatching Services Based on Pushdown Model Checking

Hsin-Hung LIN  Toshiaki AOKI  Takuya KATAYAMA  

IEICE TRANSACTIONS on Information and Systems   Vol.E95-D   No.7   pp.1882-1893
Publication Date: 2012/07/01
Online ISSN: 1745-1361
DOI: 10.1587/transinf.E95.D.1882
Print ISSN: 0916-8532
Type of Manuscript: PAPER
Category: Data Engineering, Web Information Systems
service adaptation,  behavior mismatch,  pushdown model checking,  unbounded messages,  

Full Text: PDF>>
Buy this Article

In this paper, we introduce an approach of service adaptation for behavior mismatching services using pushdown model checking. This approach uses pushdown systems as model of adaptors so that capturing non-regular behavior in service interactions is possible. Also, the use of pushdown model checking integrates adaptation and verification. This guarantees that an adaptor generated by our approach not only solves behavior mismatches but also satisfies usual verification properties if specified. Unlike conventional approaches, we do not count on specifications of adaptor contracts but take only information from behavior interfaces of services and perform fully automated adaptor generation. Three requirements relating to behavior mismatches, unbounded messages, and branchings are retrieved from behavior interfaces and used to build LTL properties for pushdown model checking. Properties for unbounded messages, i.e., messages sent and received arbitrary multiple times, are especially addressed since it characterizes non-regular behavior in service composition. This paper also shows some experimental results from a prototype tool and provides directions for building BPEL adaptors from behavior interface of generated adaptor. The results show that our approach does solve behavior mismatches and successfully capture non-regular behavior in service composition under the scale of real service applications.