简单的模型检查工具

Question

是否有简单的模型检查工具。我计划实现一个模型检查工具，它将分析一些预定义属性的代码。

Answer 1

一个重要的工具是使用Promela语言 SPIN 。如果您使用LaTeX，还有 TLA + 。

这些不会分析您的代码，但会让您表达您的假设和状态转换的模型，然后分析无效状态。换句话说，它们将检测模型中的问题，而不是模型的实现。

我看过 Goanna 的演示，但我不知道知道它是否可用（商业或其他）;这具有实际分析源代码的优势。

只要再看一下你的问题以及你问题中的评论，听起来你应该首先阅读一些文献。也许，旋转模型检查器，或指定系统（可从 Leslie Lamport的网站）。您需要重新构建问题，这样才不会尝试解决暂停问题。

Answer 2

CBMC 是一个我知道的简单工具实际操作代码。一般来说，模型检查是一个经过深入研究的领域，但是正如人们已经评论过的那样，这种广度使得很难用所提供的信息提出建议。有成千上万的SAT解算器，HDL /状态机验证的正式工具，以及大量商用静态源分析器。

无论如何，CBMC是一个很好的工具，但不要相信我的意思;这项工作背后的主要教员埃德克拉克今年赢得了图灵奖; - ）