论文标题
灵活多部分会话协议的逐项设计 - 扩展版本
Design-by-Contract for Flexible Multiparty Session Protocols -- Extended Version
论文作者
论文摘要
编排模型支持分布式编程中的正确性原则。此外，它们可以从所需系统行为的全局规范中自动生成正确的基于消息的通信模式。在本文中，我们扩展了编舞自动机理论，这是一个基于有限状态自动机的编舞模型，具有两个关键特征。首先，我们允许参与者仅在编舞自动机描述的某些场景中行动。尽管这似乎很自然，但文献中的许多编舞方法尤其是编舞自动机，禁止这种行为。其次，我们将通讯装备有限制可以传达的值的断言，从而实现逐项合同的方法。我们提供了一个工具链，允许利用上述理论以生成API进行打字稿Web编程。通过生成的API进行通信的程序随后通过构造规定的通信模式，并且没有沟通错误，例如僵局。
Choreographic models support a correctness-by-construction principle in distributed programming. Also, they enable the automatic generation of correct message-based communication patterns from a global specification of the desired system behaviour. In this paper we extend the theory of choreography automata, a choreographic model based on finite-state automata, with two key features. First, we allow participants to act only in some of the scenarios described by the choreography automaton. While this seems natural, many choreographic approaches in the literature, and choreography automata in particular, forbid this behaviour. Second, we equip communications with assertions constraining the values that can be communicated, enabling a design-by-contract approach. We provide a toolchain allowing to exploit the theory above to generate APIs for TypeScript web programming. Programs communicating via the generated APIs follow, by construction, the prescribed communication pattern and are free from communication errors such as deadlocks.
