问题标签 [model-checking]

我正在使用 UPPAAL 模型检查器在门级对同步电路进行建模，我对如何对时钟建模有些困惑，我的目标是验证不违反建立时间和保持时间。我发现一些模型在 appal 模型检查器中将时钟作为测试向量，例如 at=10 相当于上升沿，而 at=20 是下降沿，这使它看起来更像一个测试向量。任何人都可以提出一个关于如何在 UPAAL 中模拟同步电路的基本示例吗？

谢谢

我如何在不使用和例如的情况下实现symbolic executionfor ？我需要有关它的详细信息。例如，我可以通过什么语言来实现这个符号执行以及我需要知道的其他事情？particular languagemodel checkingFinite State Machine (FSM)notJava Path Finder

我正在使用 LTL 来定义开放交互协议的规则。然后我想检查一个特定的交互是否遵循规范，或者是否有任何规则被破坏。我的直接方法是使用 NuSMV，但问题是我没有要检查的交互模型，而只有一个特定的有限迹线（所有状态下所有变量的值）。

有什么方法可以在 NuSMV 中指定它吗？我基本上想输入 NuSMV 输出的模型之一作为反例：

并验证它。或者 NuSMV 是不是这个错误的工具？

谢谢！

我对 SPIN 和 Promela 还很陌生，当我尝试验证模型中的 liveness 属性时遇到了这个错误。

错误代码：

该代码基本上是彼得森算法的实现，我检查了安全性，它似乎是有效的。但是，每当我尝试使用 ltl {[]((wait -> <> (cs)))} 验证 liveness 属性时，都会出现上述错误。我不确定他们的意思，所以我不知道如何继续......

我的代码如下：

似乎 Promela 初始化了每个变量（默认为 0，或声明中给出的值）。

如何声明由未知值初始化的变量？

文档建议if :: p = 0 :: p = 1 fi但我认为它不起作用：Spin 仍然验证此声明

（并伪造p）

那么 的语义究竟是什么init？还有一些“预初始”状态？我怎样才能解决这个问题 - 而不是让我的学生感到困惑？

我想将延迟的 SystemVerilog 断言转换为形式验证器的 invarspec。合成器在下面的代码行中给出 ##1 的语法错误。

有几个属性需要验证并且有延迟。我目前正在尝试使用合成器将它们转换为正式（SMV）模型规范，该合成器适用于不涉及延迟的属性。我可以为这个正式的验证工具建模延迟吗？如果是这样，怎么做？

考虑以下Promela两个操纵共享变量的进程的模型N：

当两个过程都结束时，我如何使用LTL formula来找出变量可以具有的最小值？N

我用 UPPAAL 建立了一个模型，并使用验证器检查死锁。答案是：物业不满意。因此存在死锁。

UPPAAL 中是否有办法报告有关死锁的更详细信息，例如特定情况下所有变量的状态和当前值？

ltl p {(Xq) || (Fp)},

这个 LTL 公式接受的正式语言是什么？

例如：ltl p { p && (Xq)}

我在 UPPAAL 中模拟了两个触发器的定时模型，当我尝试验证一些属性时，我达到了 6M 状态并且我的笔记本电脑内存不足，消耗了大约 5Go，谁能告诉它是 UPPAAL 可以的近似状态数处理 ？以及在 UPPAAL 中处理状态爆炸的可能技术是什么？
谢谢