形式化编排语言理论

我们引入一种基于形式语言的元模型，称为形式化编排语言，以研究消息传递系统。我们的框架允许我们推广文献中的标准构造并对其进行对比。特别地，我们考虑全局视图、局部视图以及从前者到后者的投影等概念。从全局视图投影出的局部视图的正确性以闭包性质来刻画。我们考虑若干通信性质——如（死）锁自由——并给出形式化编排语言为保证这些性质所需满足的条件。最后，我们展示形式化编排语言如何捕获现有的形式化方法；具体地，我们考虑通信有限状态机、编排自动机和多方会话类型。值得注意的是，形式化编排语言与文献中大多数方法不同，可以自然地建模表现出非正则行为的系统。