一种Web服务编排中的可实现局部逻辑
A Local Logic for Realizability in Web Service Choreographies
摘要：
Web服务编排指定了服务之间可观察交互的条件。这方面的一个重要问题是可实现性：给定一个编排C，是否存在一组符合C的服务实现I？此外，如果C是可实现的，是否有一种算法来构造I中的实现？我们提出了一个本地的时序逻辑，其中编排可以指定，并在逻辑规范，我们解决了可实现性问题，通过构建服务实现（当它们存在时）作为通信自动机。这些是具有耦合关系的非确定性有限状态自动机。我们还报告的实现算法和讨论的实验结果。
英文摘要：
Web service choreographies specify conditions on observable interactions among the services. An important question in this regard is realizability: given a choreography C, does there exist a set of service implementations I that conform to C ? Further, if C is realizable, is there an algorithm to construct implementations in I ? We propose a local temporal logic in which choreographies can be specified, and for specifications in the logic, we solve the realizability problem by constructing service implementations (when they exist) as communicating automata. These are nondeterministic finite state automata with a coupling relation. We also report on an implementation of the realizability algorithm and discuss experimental results.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
