We introduce a meta-model based on formal languages, dubbed formal choreographic languages, to study message-passing systems. Our framework allows us to generalise standard constructions from the literature and to compare them. In particular, we consider notions such as global view, local view, and projections from the former to the latter. The correctness of local views projected from global views is characterised in terms of a closure property. We consider a number of communication properties -- such as (dead)lock-freedom -- and give conditions on formal choreographic languages to guarantee them. Finally, we show how formal choreographic languages can capture existing formalisms; specifically we consider communicating finite-state machines, choreography automata, and multiparty session types. Notably, formal choreographic languages, differently from most approaches in the literature, can naturally model systems exhibiting non-regular behaviour.
翻译:我们采用了一种基于正式语言的元模,称为正式舞蹈语言,以研究传递信息系统。我们的框架使我们能够从文献中归纳标准结构并进行比较。特别是,我们考虑全球观点、当地观点以及前者到后者的预测等概念。从全球观点中预测的当地观点的正确性以封闭属性为特征。我们考虑一些沟通特性 -- -- 例如(死)自由锁锁 -- -- 并为正式舞蹈语言提供条件,以保障这些特性。最后,我们展示了正式舞蹈语言如何能捕捉到现有的形式主义;我们特别考虑交流限定状态机器、舞蹈摄影自动成像和多功能交会话类型。值得注意的是,正式的舞蹈语言不同于文献中的大多数方法,能够自然地展示非常规行为的模式系统。