论文标题
对双重悬而未决的基于协议的系统的有限验证
Bounded Verification of Doubly-Unbounded Distributed Agreement-Based Systems
论文作者
论文摘要
分布式协议协议协议的无处不在，例如共识，已经激发了对验证此类协议以及在其顶部构建的申请的兴趣。然而，这种系统的复杂性和无限制使它们的验证一般而言，尤其是完全自动化的尤其令人难以置信。一个令人兴奋的，最近的突破表明，通过仔细的建模，可以验证有趣的分布式协议（DAB）系统，这些系统在过程数量中无限，可以减少以模型检查小型，有限的状态系统。 对于双重毫无用处的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.
