model-checking

-1热度

1回答

我正在开发一阶逻辑模型。我想证明它是一致的。可能吗？有没有我可以用来做这件事的免费工具？或者这是不可能的，因为哥德尔定理？此致敬礼。

1热度

1回答

我正在研究一个相当简单的promela模型。使用两个不同的模块，它充当人行横道/交通灯。第一个模块是输出当前信号的交通灯（绿色，红色，黄色，待定）。该模块还接收作为输入的称为“行人”的信号，该信号用作行人想穿过的指示器。第二个模块充当人行横道。它接收来自交通灯模块的输出信号（绿色，黄色，绿色）。它将行人信号输出到交通灯模块。这个模块简单地定义行人是否在穿越，等待或不在场。我的问题是，一旦计数值达到

1热度

1回答

使用NuSMV进行模型检查

确实在NuSMV中没有像NULL，Nil，None这样的值吗？而且我们不应该为过程建立模型，因为模型应该重复电子电路？我的方案是我有一个UART连接器，一个主存储器和一个进程，后者读写主内存并读写UART。在主存中有数据名为K，应该保持不变。我们想证明，如果过程不写入K' then the value of K`等于它的下一个值。我在想我的模型是否足够精细，或者太抽象了。另外如果我使用正确的

1热度

1回答

是否有选项可以提高NuSMV在规范运行期间可以使用的内存量？

在nusmv规范运行过程中，它需要几个小时，最终导致“死亡9”的结果。如何加快执行速度？是否有选项可以提高NuSMV在规范运行期间可以使用的内存量？

0热度

1回答

给定状态空间上的静态部分降阶

大多数关于部分降阶的论文都假定要分析的系统是作为一个组合运算符的一组进程给出的。这很有意义，因为您不希望首先计算状态空间，然后使用部分降阶来减少它。但是，假设你已经给出了一个平坦的状态空间，你仍然可以使用部分降阶来减少它吗？我认为这应该可以使用修改后的DFS。一些属性可以在本地检查，并且可以通过使用关于堆栈状态的信息来考虑周期条件。是否有任何纸张或其他参考提供这种算法？

2热度

1回答

可达状态数量不同的原因

我用这段代码验证了一个8位加法器。当我打印时，如果主模块为空，则可达状态的数量为1，如果包含整个主模块，则为2^32。报告可达状态数量的差异是什么？对于4位加法器，所报告的可达状态数是2^16。如果n是位数，输入状态是2^n似乎是合乎逻辑的。其他所有州从哪里来？我注意到当我添加行数a : adder (in1, in2);时，状态会增加，但这只是通过实验证实，这是增加状态数量而不是加法器模块本身。

0热度

1回答

如何在NuSMV中定义全局常量？

我不知道如何在NuSMV声明全局常量，在某种程度上类似于 #define n 5 在C。我如何在NuSMV中做到这一点？

1热度

1回答

为什么promela模型会超时？

1热度

1回答

NuXMV使用实数

我正在使用nuXmv在我正在开发的工作上，我遇到了使用Reals的麻烦。 Supose我有计划： MODULE main VAR t : Real; r : 0..5000; ASSIGN init(t):=0; init(r):=0; TRANS case r>=500 :next(r)=0 & next(t)=0 & r

2热度

1回答

你如何阅读一组原子命题？

我给出了原子命题{a，b，c}的上述系统。然后，我打算说某些LTL公式是否成立（如♢☐c）。我了解LTL公式的含义（最终永远保持c），但我不知道如何阅读该图并将其与LTL关联起来。我假设它就像一个流程图，我们从左上角开始，/{a}，可以通过不同的状态。但是它们每个意思除以a？