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.
翻译：在分布式编程中,舞蹈模型支持一个按部就班的正确性原则。此外,这些模型还能够根据理想系统行为的全球规格自动生成正确的基于信息的通信模式。在本文件中,我们扩展了舞蹈自制模型理论,这是一个基于有限状态自制模型的舞蹈模型,有两个关键特征。首先,我们允许参与者仅在舞蹈自制图案描述的某些情景中采取行动。虽然这看起来自然,但文献中的许多舞蹈方法,特别是舞蹈自制图案,禁止这种行为。第二,我们为通信配备了限制可传达的价值观的词句,使得能够逐项设计。我们提供了一个工具链,允许利用上述理论为类型自制系统网络编程生成API。通过生成的APIs进行沟通的程序,通过构建,遵循规定的通信模式,并不受诸如僵局等通信错误的影响。
相关内容
微信扫码咨询专知VIP会员