论文标题
TLA+中分布式协议的简单而简单的电感不变性推断
Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+
论文作者
论文摘要
我们提出了一种新技术，用于自动推断在TLA+中指定的参数化分布式协议的电感不变。我们的是第一个不变的推理技术，直接在TLA+上工作，TLA+是一种表现力的高级规范语言。为了实现这一目标，我们提出了一种新的不变推理算法，该算法基于一种核心程序，用于产生普通的，潜在的非诱导引理不变性，该过程被用作整体诱导不变性的候选相结合。我们将其与贪婪的引理不变的选择程序进行了选择，该过程选择了引理，以消除在我们的推理过程的每一轮中最多的反示例。我们已经在工具中实施了算法，并在各种分布式协议基准上进行了启用，并将其评估，并证明了竞争性能和唯一解决工业规模重新配置协议的能力。
We present a new technique for automatically inferring inductive invariants of parameterized distributed protocols specified in TLA+. Ours is the first such invariant inference technique to work directly on TLA+, an expressive, high level specification language. To achieve this, we present a new algorithm for invariant inference that is based around a core procedure for generating plain, potentially non-inductive lemma invariants that are used as candidate conjuncts of an overall inductive invariant. We couple this with a greedy lemma invariant selection procedure that selects lemmas that eliminate the largest number of counterexamples to induction at each round of our inference procedure. We have implemented our algorithm in a tool, endive, and evaluate it on a diverse set of distributed protocol benchmarks, demonstrating competitive performance and ability to uniquely solve an industrial scale reconfiguration protocol.
