一种按设计可用的通信系统理论

编排式编程是一种编程语言设计方法，可驱动分布式系统中错误安全协议开发。从全局规约（编排）出发，可以生成分布式实现。这种自顶向下方法的优势在于按设计即正确的原则，即从编排生成的实现（端点）按照编排中描述的严格控制流运行，且不会死锁。受信息物理系统（CPS）中具有挑战性的场景启发，我们研究编排式编程如何适应并非所有端点都始终可用的动态基础设施。我们引入全局质量演算（GC_q），这是一种编排式编程的变体，用于描述通信系统中某些参与通信的组件可能发生故障的场景。GC_q 具有用于多方、部分和集体通信的新型算子。本文研究故障感知通信的本质：首先，我们介绍 GC_q 的语法、语义及其使用示例。编排中故障与集体通信的相互作用可能导致编排因资源缺失而无法推进。作为第二个贡献，我们提供一个类型系统，确保编排在可用性条件变化的情况下仍可实现。GC_q 中的规约在与全局（会话）类型配对时，指导分布式端点的实现。第三个贡献提供了一种基于端点投影的方法，用于生成故障感知的分布式进程。我们证明了投影的正确性，以及带有可用性考虑的类型良好的编排享有可推进性。