c++ - 简单的模型检查工具

Question

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

score 5 · Accepted Answer

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

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

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

看看你的问题，再看看你问题中的评论，听起来你真的应该先阅读一些文献。也许，旋转模型检查器，或指定系统（可从Leslie Lamport 的网站下载）。你需要重新定义你的问题，这样你就不会试图解决停机问题。

score 2 · Accepted Answer

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

无论如何，CBMC 是一个很好的工具，但不要相信我的话；这项工作的主要教员 Ed Clarke 今年获得了图灵奖 ;-)

2 回答 2