QuickSilver: modeling and parameterized verification for distributed agreement-based systems
QuickSilver: modeling and parameterized verification for distributed agreement-based systems
复制标题
QuickSilver：基于分布式协议的系统的建模和参数化验证
DOI：
10.1145/3485534
复制
发表时间：
2021
影响因子：
--
通讯作者：
Samanta, Roopsha
中科院分区：
文献类型：
--
作者：
Jaber, Nouraldin;Wagner, Christopher;Jacobs, Swen;Kulkarni, Milind;Samanta, Roopsha
在过去的十年里，已经引发了一些勇敢的努力，在演绎验证分布式协议，如共识和领导者选举。奇怪的是，超出核心协议和建立在协议协议之上的目标应用程序的核查工作要少得多。这是不幸的，因为基于协议的分布式服务（如数据存储，锁和分类账）无处不在，并且可能允许模仿其模块化设计的模块化，可扩展的验证方法。我们通过我们的新的建模和验证框架，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.
登录
查看更多内容
TLC：分布式组件的时序逻辑
影响因子：
--
作者：
Griffin, Jeremiah;Lesani, Mohsen;Shadab, Narges;Yin, Xizhe
通讯作者：
Yin, Xizhe
影响因子：
22.7
作者：
LIPTON, RJ
通讯作者：
LIPTON, RJ
基于领导者选举协议的分布式协作监控系统
DOI：
10.1049/iet-wss.2015.0030
发表时间：
2016
期刊：
IET Wirel. Sens. Syst.
影响因子：
--
作者：
Che;Jichiang Tsai
通讯作者：
Jichiang Tsai
分布式协议的自动合成
DOI：
10.1145/3061640.3061652
发表时间：
2017
期刊：
SIGACT News
影响因子：
--
作者：
R. Alur;S. Tripakis
通讯作者：
S. Tripakis
通过机器人网络中的领导者选举来稳定集群
DOI：
10.1007/978-3-540-76627-8_7
发表时间：
2007
期刊：
ArXiv
影响因子：
--
作者：
D. Canepa;M. Potop
通讯作者：
M. Potop