一句话：用自动机形式化描述服务契约，并在同步/异步多主体组合中构造编排器以保证请求满足。
论文提出一种以自动机形式描述服务契约的方法。核心关注多主体组合时的基本性质：每个主体的请求都得到满足，从而使整体组合达到目标。针对请求同步或异步满足两种情形，论文在静态时刻构造编排器，使其要么产出满足所需性质的组合服务，要么检测应对违规负责的主体。为处理异步情形，方法借助线性规划技术。最后，作者将所提出的自动机与两种基于逻辑的契约规约方法建立关联。
An approach to the formal description of service contracts is presented in terms of automata. We focus on the basic property of guaranteeing that in the multi-party composition of principals each of them gets his requests satisfied, so that the overall composition reaches its goal. Depending on whether requests are satisfied synchronously or asynchronously, we construct an orchestrator that at static time either yields composed services enjoying the required properties or detects the principals responsible for possible violations. To do that in the asynchronous case we resort to Linear Programming techniques. We also relate our automata with two logically based methods for specifying contracts.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{BasileDF16,
title = {Automata for Specifying and Orchestrating Service Contracts},
author = {Davide Basile and Pierpaolo Degano and Gian-Luigi Ferrari},
journal = {Logical Methods in Computer Science},
volume = {Volume 12, Issue 4},
year = {2017},
doi = {10.2168/lmcs-12(4:6)2016}
}