English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

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. key words: service adaptation, behavior mismatch, pushdown model checking, unbounded messages

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