容错分布式算法安全性与活性验证的短反例性质
计算机科学中的逻辑
2016-11-10 v2 分布式、并行与集群计算
摘要
分布式算法在从嵌入式系统和复制数据库到云计算的许多任务关键型应用中都有使用。由于异步通信、进程故障或网络失效，这些算法难以设计和验证。许多算法通过使用阈值守卫来实现容错，例如，确保一个进程等待直到收到大多数对等进程的确认。因此，面向容错分布式系统的领域特定语言为阈值守卫提供了语言支持。我们引入了一种自动化方法，用于在进程数量和故障进程比例为参数的系统中对阈值守卫分布式算法的安全性和活性进行模型检测。我们的方法基于一个短反例性质：如果一个分布式算法违反了时序规约（在LTL的一个片段中），则存在一个长度有界且与参数无关的反例。我们通过(i)根据时序公式的结构刻画执行，以及(ii)利用转换的可交换性来加速和缩短执行，证明了这一性质。我们用我们的技术扩展了ByMC工具集（Byzantine Model Checker），并验证了10个著名的容错分布式算法的活性和安全性，其中大多数是现有技术无法处理的。
引用
@article{arxiv.1608.05327,
title = {A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms},
author = {Igor Konnov and Marijana Lazic and Helmut Veith and Josef Widder},
journal= {arXiv preprint arXiv:1608.05327},
year = {2016}
}
备注
16 pages, 11 pages appendix