发表机构
Nadi Research Institute; Faculty of Computer Science, University of Namur（纳迪研究所; 南纳慕尔大学计算机学院）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对Bach协调语言验证仅支持可达性分析的局限，提出Bach到mCRL2的自动翻译框架，显式建模共享空间，结合mu-演算实现动作与状态性质统一验证。
AI 中文摘要
尽管已有大量研究关注基于数据的协调语言的理论与实现，但其使用模型检测技术进行自动化验证的关键方面仍未得到充分探索，而这对于确保分布式系统的可靠性与正确性至关重要。现有工具（如Anemone）为Bach程序基于可达性的验证提供了坚实基础。虽然这些工具能有效分析以状态可达性表达的性质，但将支持扩展到更具表达力的时序规范——如活性性质或关于共享空间内容的不变量——仍是一个开放的机会。此类扩展对于捕获全面的系统行为非常重要，例如确保“请求总能得到响应匹配”或“消息不会静默丢失”。针对这一局限，我们提出了一种从Bach到mCRL2的自动化翻译方法，该方法显式表示共享空间，从而能够利用mCRL2的mu-演算模型检测器验证超越简单可达性的复杂性质。作为该翻译的补充，我们引入了一种系统方法，通过在mu-演算中直接表达关于共享空间内容的性质，来分析mCRL2中共享空间的数据可达性，从而为验证提供更清晰的框架。该方法实现了一种新颖的验证流程，将基于动作的性质与基于共享空间内容的状态性质相结合，这是当前协调语言验证方法中 largely 未被探索的领域，提供了新的分析维度。
英文摘要
Although significant research has focused on the theory and implementation of data-based coordination languages, the critical aspect of their automated verification using model-checking techniques remains underexplored, which is essential for ensuring reliability and correctness in distributed systems. Existing tools, such as Anemone, provide a solid foundation for reachability-based verification of Bach programs. While they effectively analyze properties expressed in terms of state attainability, extending support to more expressive temporal specifications-such as liveness properties or invariants over shared space contents-remains an open opportunity. Such extensions are important to capture comprehensive system behaviors, for instance, ensuring that "a request is always matched by a response" or that "no message is silently lost". Addressing this limitation, we propose an automated translation from Bach to mCRL2, which explicitly represents the shared space, thereby enabling the use of mCRL2's mu-calculus model checker to verify complex properties beyond simple reachability. Complementing this translation, we introduce a systematic method to analyze the shared space in mCRL2 concerning data reachability, by directly expressing properties over the shared space's contents in the mu-calculus, thus providing a clearer framework for verification. This approach enables a novel verification process that combines action-based properties with state-based properties over the shared space contents, a largely unexplored area in current coordination-language verification approaches, offering a new dimension of analysis
CommentsIn Proceedings ICE 2026, arXiv:2609.30353
Journal refEPTCS 453, 2026, pp. 59-78
