服务编排的分布式强制实施

现代面向服务的系统通常通过复用并组合分布在互联网上的现有服务来构建。服务编排(service choreography)是一种可能的服务组合形式，其目标是从全局视角规定参与服务之间的交互。本文中，我们形式化了一种用于服务编排的分布式与自动化强制实施的方法，并证明了其相对于所指定编排实现的正确性。该形式化方法作为基于模型的工具链的一部分实现，该工具链发布用于支持EU CHOReOS项目内基于编排的系统开发。我们在一个分布式社会邻近网络场景上演示了我们的方法的工作。