基于双无界分布式验证系统的有界验证
Bounded Verification of Doubly-Unbounded Distributed Agreement-Based Systems
摘要：
分布式协议（如共识）的普遍存在激发了人们对验证此类协议以及构建在其上的应用程序的兴趣。然而，这类系统的复杂性和不受约束性使得它们的核查一般来说是繁重的，特别是对于完全自动化来说是令人望而却步的。一个令人兴奋的，最近的突破表明，通过仔细的建模，它成为可能的验证有趣的分布式协议为基础的（DAB）系统，这是无限的进程数量，减少到模型检验的小，有限状态系统。这是一个悬而未决的问题，如果这样的减少也是可能的DAB系统是双重无界的，特别是DAB系统，另外有无界的数据域。我们肯定地回答这个问题，在这项工作中的DAB系统的模型，从而扩大了类DAB系统，可以自动验证。我们提出了一种新的基于简化的方法，并开发了一种工具，金星，可以有效地验证复杂的DAB系统模型。
英文摘要：
The ubiquity of distributed agreement protocols, such as consensus, has galvanized interest in verification of such protocols as well as applications built on top of them. The complexity and unboundedness of such systems, however, makes their verification onerous in general, and, particularly prohibitive for full automation. An exciting, recent breakthrough reveals that, through careful modeling, it becomes possible for verification of interesting distributed agreement-based (DAB) systems, that are unbounded in the number of processes, to be reduced to model checking of small, finite-state systems. It is an open question if such reductions are also possible for DAB systems that are doubly-unbounded, in particular, DAB systems that additionally have unbounded data domains. We answer this question in the affirmative in this work for models of DAB systems, thereby broadening the class of DAB systems which can be automatically verified. We present a new symmetry-based reduction and develop a tool, Venus, that can efficiently verify sophisticated DAB system models.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
