Automated Adaptor Generation for Services Based on Pushdown Model Checking
Automated Adaptor Generation for Services Based on Pushdown Model Checking
复制标题
DOI：
10.1109/ecbs.2011.33
复制
发表时间：
2011-04
期刊：
影响因子：
--
通讯作者：
Hsin-hung Lin;Toshiaki Aoki;T. Katayama
中科院分区：
文献类型：
--
作者：
Hsin-hung Lin;Toshiaki Aoki;T. Katayama
服务适配是解决服务组合不匹配的一种很有前途的解决方案，它通过引入称为适配器的中介服务来协调服务的交互。在之前的工作中，提出了一种使用模型检查的非常规服务适应方法来解决行为不匹配问题。该方法使用下推自动机作为适配器的行为模型，以便可以捕获服务的非常规交互。此外，使用模型检查将适配和验证集成在一起，并且可以自动生成适配器，而无需指定适配合同。然而，尽管该方法保证了行为不匹配，但我们发现通常有几个或更多满足此标准的候选者，并且可能需要根据其他要求进一步选择。本文遵循该方法并重点关注有助于自动生成适配器的要求。由于使用下推系统模型，我们对与无界消息相关的属性特别感兴趣，即消息被任意多次发送和接收，这些属性表征了服务组合中的非规则行为。本文还展示了原型工具的实验结果，以及通过我们的方法生成适配器行为后构建 BPEL 适配器的指导。
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.