25

正如标题所说，Coq 可以用作模型检查器吗？我可以将模型检查与 Coq 证明混合使用吗？这是平常的吗？谷歌谈论“微积分”，有没有人有这方面的经验或类似的东西？是否建议以这种方式使用 Coq，还是应该寻找其他工具？

4

3 回答 3

28

像Coq这样的证明助手将验证您的证明是否可靠，并且您提出的任何定理都可以（或不能）使用公理和先前证明的结果推导出来。它还将为您提出证明步骤提供支持，以减少您为解除证明而付出的努力。

相比之下，模型检查器象征性地枚举规范的状态空间并确定是否违反了任何验证条件。在这种情况下，它将提供错误跟踪，显示哪些状态更改序列将触发违规。

这些通常具有非常不同的后端处理要求，但是，虽然它们可以组合成一个工具，但 Coq 证明者似乎没有这样做。

Leslie Lamport 开发了动作时序逻辑(TLA+) 规范语言，以及配套的TLA+ 证明系统(TLAPS)，用于推理大型形式规范。它已使用PlusCal算法语言进行了扩展，该语言支持对转换为 TLA+ 表示的算法进行模型检查。

µ-演算是一种符号，用作许多形式方法方法的低级基础。您还应该查看布尔可满足性问题以获得更强力的方法。定理证明者的设计通常更加复杂，并使用传统的专家系统/人工智能概念以及专家定义的证明规则库来提供履行证明义务所需的支持。

作为证明工具的另一个示例，您可以查看Event-B 方法和随附的罗丹开发平台。这将在细化规范时更具体地确定证明义务并尝试机械地解除这些义务，而将困难的事情留给您去做。

对于模型检查，您可以查看：

在免费提供的选择中。

于 2014-03-23T11:54:25.063 回答
6

为了补充@Pekka 的现有答案，µ-calculus 是一种用于讨论固定点的符号，它表示可达性问题的解决方案。

  • 最小固定点 (μ) 的一个示例是从某处（例如，从程序的第一行）开始可以达到的最大状态集。它是一个“最小”的固定点，因为它可能是其他固定点中最小的。它是通过从空集开始并添加状态直到达到固定点来获得的。在某些条件下，固定点的存在由Knaster-Tarski定理保证。

  • 最大固定点 (ν) 的一个示例是我们可以保留在其中而不会违反某些安全要求的最大集合。它是一个“最大”的固定点，因为它是通过从所有状态的集合开始（因此，从上面以子集关系定义的集合的偏序）开始，并迭代地限制它，直到我们到达一个固定点。最大不动点是最小不动点的对偶，因此相同的定理适用于存在性和唯一性。将图搜索视为另一个示例。

通过在 μ-演算公式中交替使用固定点的类型，我们可以表达如下的时间行为：“我希望您继续在两个位置之间来回走动”，或“我希望服务器最终继续响应它收到的每个请求”。

然后，我们可以模型检查（使用枚举或符号模型检查器）我们描述的属性是否被我们设计的系统所暗示。

  • SPIN是一个枚举模型检查器：它将它探索的每个状态存储在一个哈希表中，并包含一些算法来识别它不需要枚举所有状态，但可以将其中一些状态视为其他状态的代表（来自从被验证的属性的角度来看，这些状态是等价的，因此仅对其中一个状态进行推理就足够了）。这些方法称为偏序减少。

  • NuSMV是一个符号模型检查器。它仍然会搜索系统的状态，但不会在内存中一一表示。相反，它跟踪状态集，将这些状态集表示为二元决策图。这些数据结构可以保持很小，即使它们表示带有10**24状态的集合。不过有保证。不幸的是，它们的大小仍然会爆炸，遗憾的是，对于几乎所有布尔函数（因此，几乎所有我们可能想要表示的集合）都是如此，正如Claude Shannon所证明的那样。

上述工具是为验证而设计和使用的。还有一种方法叫做综合。在研究了两者之后，它们之间是否真的有任何区别似乎令人困惑。在第一次遇到时，人们可能会认为模型和公式会有所不同。然而，这是具有欺骗性的：模型和公式作为描述方法是可以互换的，也可以混合使用。

验证和综合之间的区别在于量词的交替：

  • 验证具有统一的量化（通常都是通用的）
  • 综合具有交替量词：它涉及嵌套的存在量词和全称量词。

当然，也可以验证一个量化的公式，例如\forall x: \exists y: f(x, y)。这不就是验证吗？嗯，它证明了在问题的核心，在综合和验证之间没有任何数学差异。传统上，人们遇到的大多是上述情况，即量化如何出现在哪些问题被认为是综合，哪些问题被认为是验证。

综合和验证之间的主要真正区别在于我们如何使用检查公式是否为真的结果：

  • 在验证中，我们已经实现了我们想要的系统，并且我们检查它是否满足一些期望的属性。如果没有，我们将（手动）尝试修复实现，然后再次检查。

  • 在综合中，最终系统的某些部分我们尚未完全详细说明。我们让我们使用的工具选择该细节。换句话说，该工具以一种使公式为真的方式消除了存在量词，并告诉我们它做了什么，以便我们以这种方式完成系统，确保公式为真。

C 中的综合工具的gr1c一个示例是 .Python 中的另一个示例是omega. 还有其他几个工具。

不管你如何处理一个问题，至少要确保你写的是计划是什么，你写的是规范。

关于这些主题的最佳书籍之一是 Leslie Lamport 的指定系统。并且要说服各种表示是同一事物的面孔，请考虑阅读计算机科学和状态机。

于 2016-07-19T07:48:59.337 回答
0

有一些关于使用 Coq 作为模型检查器的工作，例如参见https://github.com/coq-contribs/smc。但是，我不知道有人在严肃的应用程序中使用过它。

于 2017-01-20T17:29:33.307 回答