alloy - 合金分析仪是“伪造者”吗？

Question

在我的社区中，最近我们积极使用正式规范的“伪造”一词。例如，该术语出现在： https ://www.cs.huji.ac.il/~ornak/publications/cav05.pdf

我想知道合金分析仪是否造假。这对我来说似乎是真的，但我不确定。这是对的吗？如果不是，有什么区别？

标签： alloy

Answer 1

是的，Alloy 是伪造者。Alloy 在 20 年前推出时的主要新颖之处在于辩称伪造通常比验证更重要，因为大多数设计都不正确，因此分析器的作用应该是发现错误，而不是表明它们不存在. 有关此问题的讨论，请参阅第 1.4 节，软件分析中的验证与反驳：路线图（Jackson 和 Rinard，2000）；第 5.1.1 节，软件抽象中的实例查找和不可判定性妥协（Jackson 2006）。

然而，在 Alloy 的案例中，还有另一个方面，即范围完整分析实际上从验证的角度来看非常有效。这种说法就是我们所说的“小范围假设”——大多数错误都可以在小范围内找到（即分析受到每种基本类型中固定数量的小元素的限制）。

顺便说一句，Alloy 是最早建议使用 SAT 进行有界验证的工具之一。例如，参见Boolean Compilation of Relational Specifications (Daniel Jackson, 1998)，这是第一篇有界模型检查论文的作者所熟知的技术报告，其中讨论了 Alloy 的前身 Nitpick，其内容如下：

Nitpick 背后的假设是一个有争议的假设。在实践中，小范围就足够了。换句话说，大多数错误都可以通过小范围内的反例来证明。这是一个纯粹的经验假设，因为相关的误差分布不能用数学来描述：它是由人们编写的规范决定的。

我们希望 Nitpick 工具的成功使用能够证明这一假设的合理性。已经有一些证据证明它的合理性。根据我们迄今为止使用 Nitpick 的经验，我们没有通过将范围扩大到 6 来获得更多信息。

类似的范围概念隐含在硬件模型检查的上下文中。尽管单个状态机通常是有限的，但设计通常由并行执行的机器数量参数化。该指标类似于范围；随着机器数量的增加，状态空间呈指数增长，几乎不可能分析一个涉及多于几台机器的系统。然而幸运的是，似乎只需要很小的配置就可以找到错误。对 Futurebus+ 缓存协议 [C+95] 的著名分析可能标志着模型检查行业声誉的转折点，最多可针对 8 个处理器和 3 个总线进行分析。然而，报告的缺陷可以通过涉及最多 3 个处理器和 2 个总线的反例来证明。