问题标签 [model-checking]

<编辑> 关于这个问题离题且过于基于意见，我会尽量说得更清楚。我的目标是不知道是否存在这样的工具，我对关于什么是最好的工具的意见不感兴趣。在我写这个问题的时候，我花了很多时间在互联网上搜索，发现只是旧的死项目，但是存在这样的 Java 工具，我不敢相信 C# 没有任何东西。我认为这个问题与编程（代码验证）有关，并不是真的在征求意见。此外，要找到这些信息仍然不容易，我认为我的回答可以帮助节省某人的时间。也就是说，我不是 stackoverflow 的专家，如果您仍然认为问题/答案不适合该网站，请随时删除它。< /编辑>

我找到了 Moonwalker http://fmt.cs.utwente.nl/tools/moonwalker/，但最后一次更新是在 2009 年完成的，我认为它不支持 .net4.5（而且文档记录很差）。

这个问题的答案建议将 CodeContracts 作为模型检查工具模型检查工具 c#，但我已经尝试使用它，但我认为它并不是一个模型检查器，与 Java Path Finder for Java 的方式不同。我穿了吗？可以像 JPF 一样使用吗？

我需要能够知道代码的某个部分是否以可能死锁的方式设计。假设这是学校的事情，即使我确定我的代码正在运行，我也必须对它进行模型检查。（是的，我们被允许并鼓励在互联网上查看）。

我正在研究关于 Graph Grammar Modeling（模型检查）的研究论文。为了更好地理解，我开始探索研究人员进行的实验。

他们使用点符号来指定图形结构并使用属性，例如labelangle=-35和type = "rt|re|node"

我在互联网上找不到任何关于点语言的好的参考资料，它们都不是从新手的角度开始的。当我搜索 stackoverflow 时，我感觉没有标准的方式来指定 dot 中的内容，因为一些符号已经过时但仍然存在于文献中。

有人可以向我解释属性的目的是什么，type或者labelangle至少在这种情况下。

注意：graphviz 生成的图形似乎也type没有区别。labelangle

例如，考虑下图，它在第 58 页的拓扑形成的详细描述中被引用为坏模式（不要担心坏模式是什么，这是研究人员在他们的论文中定义的），使用这个点文件创建：

根据我到目前为止的理解，我什至不确定这个图应该是上面点文件的输出，因为边和节点映射与点文件和输出图中指定的不一样。

请帮忙。

对于以下代码，

我收到以下错误，

为什么呢？Promela 不应该为 cond1 的每个值执行（cond1 == 0 和 cond1 != 0）。至少这是这里写的。

在验证期间，不会进行此类调用，因为在此模式下将有效地探索所有行为选项，一次一个。

以下是导致此问题的代码。

如果我在第一个条件下删除了nempty调用，错误就消失了。根据我的阅读，如果在条件中使用接收或发送语句，则不能使用 else 语句，但据我所知，nempty不是发送或接收语句，而只是检查通道是否不是空的。那么，我在做什么错误，我该如何解决这个问题。

我目前正在运行我的 UPPAAL 模拟器。我的模拟器在某个时间点后停止运行代码。这一点取决于我提供的声明。但我想知道时钟什么时候停止运行？有什么东西会触发这个吗？

我目前正在写我的硕士论文，并面临着在时间逻辑中指定和验证我的方法。

在我的情况下，哪种时间逻辑最适合使用？我真的很想得到一些关于我的方法以及如何进行的反馈

我的模型由参与者组成，这些参与者将同时执行。对于每个参与者，可以注册规则。它们看起来像这样：

例如

这意味着 c 必须收到来自 b 的消息和来自 c 的消息，才能被允许向 d 发送消息。

在其中一个参与者发送或接收消息之前，我的原型会检查参与者是否被允许执行该操作。到目前为止，我想验证该算法是否执行以下操作：

1. 如果不存在其条件成立的规则：禁止该操作

2. 如果存在条件成立且禁止该操作的规则：禁止该操作

3. 如果存在条件成立的规则，则它允许该操作，并且不存在其条件成立且禁止该操作的其他规则：允许该操作

我下载了模型检查器nusmv-tools（https://code.google.com/a/eclipselabs.org/p/nusmv-tools/ ）。我在eclipse上成功安装了它及其依赖项（如xtext）并重新启动了eclipse。

现在，我希望 Eclipse 能够识别 nusmv 文件（扩展名为 '.smv'），但它不能。

我的问题是，我应该怎么做才能在 Eclipse 中解析 nusmv 文件，以便 eclipse 识别并突出显示 nusmv 文件（.smv）。

（我应该创建一个 xtext 项目还是 java 项目或通用项目？我应该将哪些库或外部 jar 添加到项目中？）

有什么帮助吗？谢谢

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

所以我在我的 Promela 代码中使用了以下行。

但是，它正在引起状态爆炸。我用以下if语句替换它，突然状态爆炸问题消失了。我上面显示的语句不select应该等同于if下面的语句吗？这里发生了什么？

当我A[] not deadlock在模型上的 Verifier 中运行查询时，验证停止并出现错误：

验证因错误而中止。这很可能是由超出范围的分配或超出范围的数组查找引起的。

这是否暗示我的模型在“超出范围的赋值或超出范围的数组查找”发生之前是无死锁的？