问题标签 [nusmv]

I'm trying to write the following model in NuSMV

In other words, z becomes bad only when x AND y are in the state bad too. This is the code I've written

But I got only these reachable states

How can I modify my code to get also

in the reachable states?

In addition, I'm not sure if I've to add or not that red arrow printed in the model picture: if x and y are in state bad, I want that for sure sooner or later also z becomes bad.

Thank you so much for helping!

我正在尝试使用 cmake 实用程序在 Ubuntu 17.04 上构建 NuSMV。

使用 cmake 工具创建 make 文件，但是当我尝试使用 make 实用程序时，它给出了错误

任何人都可以请帮忙。如何解决

我试图将 smv 模型传递给 xSAP（1.2.0 版），但出现此错误

该模型适用于 NuSMV（版本 2.6.0）。我不明白我是否必须将 xml 文件传递​​给 xSAP（如果是这样，我如何在 xml 文件中翻译 smv？）或者是否存在其他错误。

非常感谢您的帮助！

我已经从 NuSMV 网站下载了这些文件，但我实际上无法在我的系统上运行该应用程序。任何线索将不胜感激。

该文件包含文件夹 - bin、lib、share、include

我有以下简化的公钥 Needham-Schroeder 协议：

1. A → B: {Na, A} Kb
2. B → A: {Na, Nb} Ka
3. A → B: {Nb} Kb

其中Na,是, , 和Nb的随机数,分别是 的公钥。ABKaKbAB

由一方的公钥加密的消息只能由一方解密。

在步骤 (1)，A通过向 发送随机数及其身份（由B的公钥加密）来启动协议B。使用其私钥，B解密消息并获得A的身份。

在第 (2) 步，B将A's 及其随机数（由A's 的公钥加密）发送回A。使用它的私钥，A解码消息并检查它的随机数是否被返回。

在第 (3) 步，A将B的随机数（由B的公钥加密）返回给B。

这是对上述简化协议的中间主要攻击：

• (1A) A → E: {Na, A} Ke(A想和E)
• (1B) E → B: {Na, A} Kb(E想要说服B它是A)
• (2B) B → E: {Na, Nb} Ka(B返回由 加密的随机数Ka)
• (2A) E → A: {Na, Nb} Ka(E将加密消息转发给A)
• (3A) A → E: {Nb} Ke(A确认它正在与E)
• (3B) E → B: {Nb} Kb( return 的 nonceE返回B)

我希望当发现攻击时，提出一个修复来防止攻击（B将其身份与随机数一起发送回A）：

1. A → B: {Na, A} Kb
2. B → A: {Na, Nb, B} Ka（B将其身份与随机数一起发送回A）
3. A → B: {Nb} Kb

问题是：

1. 如何编写 LTL 公式和 NuSMV 模块eve来对攻击者进行建模并见证中间人攻击？
2. 如何防止攻击？

alice(A)的进程：

bob(B)的过程：

主要流程：

非常感谢！

我正在做一个程序校正/综合项目。我的任务是获取错误轨迹（反例），将其定位在完整的状态空间中，并在该位置修复模型。我想将其实现为 NuSMV 扩展。

我一直在调试 NuSMV 以了解和探索它的源代码。到目前为止，我已经找到了创建 BDD FSM 的方法（compile.c 第 520 行）。我试图找到一种遍历 bdd 的方法，以便以编程方式访问状态空间，从而对模型执行我的纠正工作。我还不能理解 NuSMV 用来通过 bdd fsm 验证属性的递归探索函数。

我想知道如何遍历 bdd 结构，以便通过 dot 等工具对其进行可视化。我还想知道是否已经制作了这样或类似的可视化（我已经搜索过但没有找到）。其次，我想验证我所采取的方向是否正确，或者是否有更好的方法来获得给定模型的完整状态空间，并探索它，特别是关于获得的反例通过 NuSMV。

现代模型检查器（如NuSMV）的近似最大状态空间大小是多少。我不需要一个确切的数字，而是一些状态大小值，运行时间仍然可以接受（比如几周）。

除了符号模型检查之外，还有哪些改进用于提高该限制？

我正在研究 NuSMV 上的河内塔问题。对于 n 个磁盘，需要 2^n - 1 个步骤。我怎样才能弄清楚NuSMV在哪个n之前是可行的？ hanoi_model

提前致谢！妮维莎

i hame fsm like this FSM

and i wrote piece of code to check LTL property on FSM this is my LTL property

my NuSMV code is

After model checking with following command i wonder when i see NuSMV return True

NuSMV result is :

but i can find CE manually after read NuSMV 2.6 User Manual i could not find which part of NuSMV code is wrong

我在 NuSMV 中有模型，在检查 ltl 规范 NuSMV 后给我一个反例是否有可能找出包含反例而不是其中之一的所有路径？