Konnov Igor, Lazić Marijana, Veith Helmut, Widder Josef
Institute of Information Systems E184/4, TU Wien (Vienna University of Technology), Favoritenstraße 9-11, 1040 Vienna, Austria.
Form Methods Syst Des. 2017;51(2):270-307. doi: 10.1007/s10703-017-0297-4. Epub 2017 Sep 20.
Automatic verification of threshold-based fault-tolerant distributed algorithms (FTDA) is challenging: FTDAs have multiple parameters that are restricted by arithmetic conditions, the number of processes and faults is parameterized, and the algorithm code is parameterized due to conditions counting the number of received messages. Recently, we introduced a technique that first applies data and counter abstraction and then runs bounded model checking (BMC). Given an FTDA, our technique computes an upper bound on the diameter of the system. This makes BMC complete for reachability properties: it always finds a counterexample, if there is an actual error. To verify state-of-the-art FTDAs, further improvement is needed. In contrast to encoding bounded executions of a counter system over an abstract finite domain in SAT, in this paper, we encode bounded executions over integer counters in SMT. In addition, we introduce a new form of reduction that exploits acceleration and the structure of the FTDAs. This aggressively prunes the execution space to be explored by the solver. In this way, we verified safety of seven FTDAs that were out of reach before.
基于阈值的容错分布式算法（FTDA）的自动验证具有挑战性：FTDA有多个受算术条件限制的参数，进程数和故障数是参数化的，并且由于对接收消息数量进行计数的条件，算法代码也是参数化的。最近，我们引入了一种技术，该技术首先应用数据和计数器抽象，然后运行有界模型检查（BMC）。给定一个FTDA，我们的技术计算系统直径的上界。这使得BMC对于可达性属性是完备的：如果存在实际错误，它总能找到一个反例。为了验证最新的FTDA，还需要进一步改进。与在SAT中对抽象有限域上的计数器系统的有界执行进行编码不同，在本文中，我们在SMT中对整数计数器上的有界执行进行编码。此外，我们引入了一种新的约简形式，它利用了加速和FTDA的结构。这极大地修剪了求解器要探索的执行空间。通过这种方式，我们验证了之前无法验证的七个FTDA的安全性。
