Formal verification of an interactive consistency algorithm for the Draper FTP architecture under a hybrid fault model

Fault-tolerant systems for critical applications should tolerate as many kinds of faults and as large a number of faults as possible, while using as little hardware as is feasible, and they should be provided with strong assurances for their correctness. Byzantine fault-tolerant architectures are attractive because they tolerate any kind fault, but they are rather expensive: at least 3m+1 processors are required to withstand m arbitrary faults. Two recent developments mitigate some of the costs: algorithms that operate under a hybrid fault model tolerate more faults for a given number of processors than classical Byzantine fault-tolerant algorithms, and asymmetric architectures tolerate a given number of faults with less hardware than conventional architectures. In this paper, we combine these two developments and present an algorithm for achieving interactive consistency (the problem of distributing sensor samples consistently in the presence of faults) under a hybrid fault model on an asymmetric architecture. The extended fault model and asymmetric architecture complicate the arguments for the correctness and the number of faults tolerated by the algorithm. To increase assurance, we have formally verified these properties and checked the proofs mechanically using the PVS verification system. We argue that mechanically supported formal methods allow for effective reuse of intellectual resources, such as specifications and proofs, and that exercises such as this can now be performed very economically