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.
翻译:在过去的十年中,在对分布式协议协议协议进行推论性核查方面,如协商一致和领导人选举等,出现了数项大胆的努力。奇怪的是,除了核心协议和在协议协议协议协议之上建立的目标应用程序之外,核查努力也少得多。这很不幸,因为基于协议的分布式服务,如数据储存、锁和分类账,无处不在,而且有可能允许模块化、可扩缩的核查方法,模仿其模块化设计。我们通过我们的新颖的建模和核查框架QuickSilver,解决了对分布式协议系统进行核查的需要。QuickSilver不仅是模块化的,而且还是完全自动化的。QuickSilver的关键功能是我们将经核实的协议协议协议的抽象编码,这些协议有助于模块化、可变和可变缩放的自动核查。我们通过建模和有效核查一系列从实际应用中改编成的复杂案例研究,例如数据储存、锁定服务、监视系统、移动机器人的路径算法等等,展示了快速Silver的潜力。