TLA +中分布式协议的简单归纳不变推理
Plain and Simple Inductive Invariant Inference for Distributed Protocols in 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
