论编排中的非确定性消解
软件工程
2023-06-22 v4 计算机科学中的逻辑
摘要
编排（Choreographies）通过消息传递指定多方交互。编排的实现是由独立进程组成的组合，这些进程的行为如编排所指定。现有编排与实现之间正确性/完备性的关系基于选择是非确定性的模型。将非确定性选择解析为确定性选择（例如条件语句）对于正确刻画编排与其具体编程语言实现之间的关系是必要的。我们引入了一种编排的可实现性概念——称为全谱实现（whole-spectrum implementation）——其中选择在编排中仍为非确定性，但在其实现中为确定性。我们的全谱实现概念排除了那些无论置于何种上下文中都绝不会遵循非确定性选择某一分支的角色的确定性实现。我们给出了一种用于检查全谱实现的类型规则。作为一个案例研究，我们在全谱实现的视角下分析了 POP 协议。
引用
@article{arxiv.1904.08337,
title = {On Resolving Non-determinism in Choreographies},
author = {Laura Bocchi and Hernan Melgratti and Emilio Tuosto},
journal= {arXiv preprint arXiv:1904.08337},
year = {2023}
}