一句话:提出新可控性概念,将监督控制的经典综合改造为服务合约自动机的编排与协同综合,并给出统一抽象算法。
本文旨在弥合监督控制理论与服务协调之间的鸿沟,把服务合约形式化为合约自动机,并对其综合编排与协同。作者修改监督控制理论中用于求取“最宽容控制器”的经典综合算法,关键在于提出新的可控性概念,使同一框架能生成编排与协同。随后提出参数化抽象综合算法,证明它统一并推广经典监督控制综合以及具体的编排、协同综合。借助该抽象综合,作者进一步表明这些具体综合处于一种细化序关系,并用服务领域的运行示例加以说明。
We present a number of contributions to bridging the gap between supervisory control theory and coordination of services in order to explore the frontiers between coordination and control systems. Firstly, we modify the classical synthesis algorithm from supervisory control theory for obtaining the so-called most permissive controller in order to synthesise orchestrations and choreographies of service contracts formalised as contract automata. The key ingredient to make this possible is a novel notion of controllability. Then, we present an abstract parametric synthesis algorithm and show that it generalises the classical synthesis as well as the orchestration and choreography syntheses. Finally, through the novel abstract synthesis, we show that the concrete syntheses are in a refinement order. A running example from the service domain illustrates our contributions.
DOI 原文 · arXiv · PDF(开放获取) · DBLP
@article{abs-1910-00849,
title = {Synthesis of Orchestrations and Choreographies: Bridging the Gap between Supervisory Control and Coordination of Services},
author = {Davide Basile and Maurice H. ter Beek and Rosario Pugliese},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 2},
year = {2020},
doi = {10.23638/lmcs-16(2:9)2020}
}