论文标题
QuickSilver：具有分布式协议（扩展版本）的系统的建模和参数化验证框架
QuickSilver: A Modeling and Parameterized Verification Framework for Systems with Distributed Agreement (Extended Version)
论文作者
论文摘要
在过去的十年中，激发了几项英勇的努力，以扣除分布式协议协议（例如共识和领导人选举）的验证。奇怪的是，验证工作超出了核心协议和目标应用程序之外的核心方案，这些核心协议和目标应用程序是协议协议协议之上的。这是不幸的，因为基于协议的分布式服务（例如数据存储，锁和分类帐）无处不在，并且可能允许模拟其模块化设计的模块化，可扩展的验证方法。 我们通过我们的新型建模和验证框架QuickSilver，不仅是模块化的，而且完全自动化的，我们解决了基于分布式协议系统的验证需求。 QuickSilver的关键促进功能是我们对经过验证的协议协议的抽象编码，这些协议协议有助于模块化，可决定性和可扩展的自动验证。我们通过建模并有效地验证一系列棘手的案例研究来证明QuickSilver的潜力，这些案例研究改编自现实世界中的应用程序，例如数据存储，锁定服务，监视系统，用于移动机器人的探路算法等等。
The last decade has sparked several valiant efforts in deductive verification of distributed agreement protocols such as consensus and leader election. Oddly, there have been far fewer verification efforts that go beyond the core protocols and target applications that are built on top of agreement protocols. This is unfortunate, as agreement-based distributed services such as data stores, locks, and ledgers are ubiquitous and potentially permit modular, scalable verification approaches that mimic their modular design. We address this need for verification of distributed agreement-based systems through our novel modeling and verification framework, QuickSilver, that is not only modular, but also fully automated. The key enabling feature of QuickSilver is our encoding of abstractions of verified agreement protocols that facilitates modular, decidable, and scalable automated verification. We demonstrate the potential of QuickSilver by modeling and efficiently verifying a series of tricky case studies, adapted from real-world applications, such as a data store, a lock service, a surveillance system, a pathfinding algorithm for mobile robots, and more.
