Coq可以(轻松)用作模型检查器吗？

Question

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

Answer 1

像Coq这样的证明助手将验证您的证明是否合理,并且您提出的任何定理都可以(或不能)使用公理和先前证明的结果得出.它还将为您提供支持,以提出证明步骤,以减少您为放置样张所需的工作量.

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

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

动作的时间逻辑(TLA +)规范语言以及伴随的TLA +证明系统(TLAPS)由Leslie Lamport开发,用于推理大型正式规范.它已经使用PlusCal算法语言进行了扩展,该语言支持对转换为TLA +表示的算法进行模型检查.

的μ-演算是用作许多形式方法的方法低电平托底一个符号.您还应该查看布尔可满足性问题,以获得更强力的方法.定理证明在设计中通常更为复杂,并使用传统的专家系统/ AI概念以及专家定义的证明规则库来提供履行证明义务所需的支持.

作为校对工具的另一个例子,您可以查看Event-B方法和随附的Rodin开发平台.当改进规范时,这将更具体地确定证明义务并试图机械地排除这些义务,留下难以做到的事情.

对于模型检查,您可以查看:

在免费提供的选择中.

Answer 2

为了补充@Pekka的现有答案，µ-calculus是谈论固定点的一种表示法，它表示可及性问题的解决方案。

最小定点（？）的示例是从某处（例如，从程序的第一行开始）可以达到的最大状态集。它是“最小”的固定点，因为它在其他固定点中最小。它是通过从空集开始并添加状态直到到达固定点来获得的。在某些条件下，Knaster-Tarski定理确保了定位点的存在。
最大定点（？）的示例是我们可以保留在里面而没有违反某些安全要求的最大集合。它是“最大”的固定点，因为它是通过从所有状态的集合开始（因此，从上面按子集关系定义的集合的部分顺序）获得的，并迭代地对其进行限制，直到到达固定点为止。最大定点是对偶定点或最小定点，因此相同的定理适用于存在性和唯一性。将图搜索视为另一个示例。

通过在？-演算公式中替换固定点的类型，我们可以表示以下时间行为：“我希望您在两个位置之间来回移动”，或“我希望服务器最终保持对收到的每个请求的响应” ”。

然后，我们可以进行模型检查（使用枚举或符号模型检查器），以确保所描述的属性是否由我们设计的系统隐含。

SPIN是一种枚举模型检查器：它将其探索的每个状态存储在哈希表中，并包括一些算法，该算法可以识别它不需要枚举所有状态，但是可以将其中一些作为其他状态的代表（从从要验证的属性的角度来看，这些状态是等效的，因此仅就其中之一进行推理就足够了。这些方法称为偏序约简。
NuSMV是符号模型检查器。它仍会搜索系统状态，但不会在内存中一个一个地表示它们。相反，它会跟踪状态集，并将这些状态集表示为二进制决策图。这些数据结构即使在用10**24状态表示集合时也可以保持很小。虽然有保证。不幸的是，它们的大小仍然会爆炸，可悲的是，几乎所有的布尔函数都是如此（因此，几乎所有我们可能要表示的集合），正如Claude Shannon所证明的那样。

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

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

当然，例如，也可以验证量化公式\forall x: \exists y: f(x, y)。这不只是验证吗？好吧，这表明合成和验证之间的本质没有任何数学差异。传统上，人们通常会遇到以上情况：量化如何出现在哪些问题被视为综合问题以及哪些问题被视为验证问题上。

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

在验证中，我们已经有了所需系统的实现，并且检查它是否满足某些所需的属性。如果没有，我们将（手动）尝试修复实现，然后再次检查。
综合而言，最终系统的某些部分尚未完全详细说明。我们使用我们使用的工具来选择细节。换句话说，该工具以使公式正确的方式消除了存在量词，并告诉我们它做了什么，以便我们以这种方式完善系统，确保公式正确。

用C语言编写综合工具的gr1c一个例子，用Python语言编写另一个例子的omega。还有其他几种工具。

但是，如果遇到问题，至少要确保编写计划是什么，编写规范是什么。

关于这些主题的最好的书之一是莱斯利·兰波特的《指定系统》。为了说服各种表示形式都是同一事物的面孔，请考虑阅读《计算机科学》和《状态机》。