Dist-Orc：基于重写的 Orc 分布式实现及其形式化分析

Orc 是一种服务编排理论，允许对分布式和定时计算进行结构化编程。目前已有多种针对 Orc 的形式语义被提出，包括由作者开发的重写逻辑语义。Orc 也有一个具备函数式编程特性的功能完备的 Java 实现。然而，与大多数分布式语言的描述一样，Orc 的形式语义与其实现之间存在着相当大的差距，即： 不容易仅通过使用 Orc 的形式语义将程序部署在分布式实现中， 在分布式 Orc 实现层面上不易进行形式化分析。在本工作中，我们克服了 Orc 的上述问题 和。具体而言，我们描述了一种基于重写逻辑和 Maude 的实现技术，该技术显著缩小了这一差距。该技术的启用特性是 Maude 通过 TCP 套接字对外部对象的支持。我们描述了如何使用套接字来实现 Orc 站点调用与返回，以及如何向 Orc 表达式和站点提供实时定时信息。随后，我们展示了如何通过定义时间和套接字通信基础设施的抽象模型，在所得的分布式实现中对 Orc 程序在合理的抽象层次上进行形式化分析，并讨论了在何种假设下该分析可被认为是正确的。最后，通过一个案例研究对该分布式实现和形式化分析方法进行了说明。