关联 Reo 连接器的形式语义模型：连接器着色与约束自动机

在过去的几十年中，协调语言应运而生，用于规范和实现通信软件组件的交互协议。这类语言包括 Reo，一个用于组合式构建连接器的平台。近年来，各种用于描述 Reo 连接器行为的形式主义相继出现，每种形式主义都有其特定的用途。自然会产生关于这些模型之间如何相互关联的问题。从理论角度来看，回答这些问题能让我们更深入地了解 Reo 的基础；而从更实际的角度来看，这些答案拓宽了 Reo 开发工具的适用范围。在本文中，我们探讨了其中一个问题：研究了着色模型与约束自动机之间的等价性，这两者是 Reo 中最主导且最具实际意义的语义模型。具体而言，我们定义了将一个模型转换为另一个模型（反之亦然）的算子，证明了它们的正确性，并表明它们在组合上是可分配的。为了确保转换算子是一一映射（而非多对一），我们用数据约束扩展了着色模型。虽然这主要是一项理论贡献，但我们勾勒了结果的一些潜在应用：拓宽现有连接器验证和动画工具的适用范围。