Distributed architectures are used to improve performance and reliability of various systems. An important capability of a distributed architecture is the ability to reach consensus among all its nodes. To achieve this, several consensus algorithms have been proposed for various scenarii, and many of these algorithms come with proofs of correctness that are not mechanically checked. Unfortunately, those proofs are known to be intricate and prone to errors. In this paper, we formalize and mechanically check a consensus algorithm widely used in the distributed controls community: the Weighted-Mean Subsequence Reduced (W-MSR) algorithm proposed by Le Blanc et al. This algorithm provides a way to achieve asymptotic consensus in a distributed controls scenario in the presence of adversarial agents (attackers) that may not update their states based on the nominal consensus protocol, and may share inaccurate information with their neighbors. Using the Coq proof assistant, we formalize the necessary and sufficient conditions required to achieve resilient asymptotic consensus under the assumed attacker model. We leverage the existing Coq formalizations of graph theory, finite sets and sequences of the mathcomp library for our development. To our knowledge, this is the first mechanical proof of an asymptotic consensus algorithm. During the formalization, we clarify several imprecisions in the paper proof, including an imprecision on quantifiers in the main theorem.
翻译:使用分布式结构来提高各种系统的性能和可靠性。 分布式结构的一个重要能力是所有节点之间达成共识的能力。 为了实现这一点,已经为各种正统控制设想提出了数种共识算法, 许多这些算法都附有未经机械检查的正确性证明。 不幸的是, 这些证明已知复杂, 容易出错。 在本文中, 我们正式化并机械地检查分布式控制群体广泛使用的协商一致算法: 由勒布兰茨等人提议的加权- MEan 子序列减缩(W- MSR)算法(W- MSR)。 这个算法提供了一种方法, 在一个分布式控制设想中, 在有各种对抗性代理人(攻击者)在场的情况下, 在分布式一致协议的基础上, 提出一些可能无法更新其状态的证据。 使用 Coq 验证助理, 我们正式化了在假设攻击者模型下实现弹性性一致所需的必要和充分条件。 我们利用了现有的Coq格式化的图表理论、 定式的套件和顺序。 我们的数学缩略图库中的第一个知识, 包括机械化的校准。