使用 大语言模型 规范引导综合无死锁通信协议细化

确保通信协议的行为正确性是分布式软件系统的一个核心挑战，因为细微的不一致可能会导致死锁。在这种情况下，协议细化（安全地替换协议以保持正确性以及与其他组件的兼容性）至关重要。 大语言模型 (LLM) 在代码生成和程序合成方面表现出了强大的能力，但缺乏可靠地产生具有正确行为的输出的机制。正式规范方法，例如多方会话类型 (MPST)，提供严格的保证，包括无死锁，但对自动构建协议细化提供的支持有限。在本文中，我们提出了 Syntropy，一个在 MPST 规范和 LLM 指导下综合协议细化的框架。它将细化约束直接合并到生成过程中，确保生成的变体满足这些保证。我们的综合评估表明，Syntropy 在保持高句法正确性的同时实现了 95.6%-99.5% 的有效性，并在多个 LLM 中产生了多样化的、重要的改进。