使用 NuSMV 进行模型检查

Question

在 NuSMV 中真的没有像 NULL、nil、None 这样的值吗？

我们不应该为流程制作模型，因为模型应该代表电子电路？

我的情况是，我有一个 UART 连接器、一个主存储器和一个进程，后者在该进程中读取和写入主存储器以及读取和写入 UART。在主内存中有名为K 的数据应该保持不变。我们想证明如果进程不写K' then the value ofK`等于它的下一个值。

我想知道我的模型是否足够细粒度或者是否过于抽象。另外，如果我使用了正确的数据类型。

MODULE UART (proc, output, input)
VAR state : {idle, receive, transmit};
    Rx : unsigned word [ 8 ]; --vector of bytes
    Tx : unsigned word [ 8 ];
ASSIGN
    next (Rx) :=
        case
            proc = read : input; TRUE : (Rx);
        esac;
    next (Tx) :=
        case
            proc = write : output; TRUE : (Tx);
        esac;
    next (state) :=
        case
            proc = write : receive; proc = read : transmit; TRUE : idle;
        esac;
TRANS
    proc != read -> next (Rx) = Rx;
MODULE MEM (proc, input, output)
VAR K : unsigned word [ 8 ]; data : array 0 .. 7 of array 0 .. 7 of unsigned word [ 8 ];
ASSIGN
    init (data[1][0]) := K; 
    next (K) :=
        case
            output = data[1][0] : output;
            TRUE : K;
        esac;
MODULE main
VAR proc : {idle, read, write}; input : unsigned word [ 8 ]; 
    output : unsigned word [ 8 ]; 
    memory : MEM (proc, input, output); 
    uart0 : UART (proc, input, output); 
ASSIGN init (input) := memory.data[0][0]; init (output) := memory.data[0][0];
LTLSPEC G (output != memory.data[1][0]) -> G (memory.K = next (memory.K))

Answer 1

在您的帖子中，您涉及许多主题，我不确定哪个是您的主要问题。

在 NuSMV 中真的没有像 NULL、nil、None 这样的值吗？

对于 C 来说，这在同样的意义上是正确的。Nil 只是给定数据类型允许的值中的一个值。看看你的例子，你似乎并不真的需要它，不是吗？

我们不应该为流程制作模型，因为模型应该代表电子电路？

没有。只要您不需要创建动态对象（例如，C 中的 malloc），您就可以表示您想要的任何内容。另一个问题是关于进程的同步性/并发性。您仍然可以为异步进程建模，但它需要显式编码调度程序。

关于代码：我没有运行它，但很多东西看起来很可疑。我建议您尝试使用 NuSMV 模拟命令来查看模型的行为。

• UART 模块：您只能同时写入 Rx 和 Tx。这些值永远不会被读取。
• UART 模块：我建议不要混合 ASSIGN 和 TRANS。这是在模型中引入死锁的简单方法。而且，你写的 TRANS 已经被 ASSIGN 包含了
• UART 模块：为什么需要 state 变量？
• MEM 模块：我不明白您为什么使用数组数组，因为您只查看两个值。我认为您可以更多地抽象这部分。从您的非正式描述来看，您似乎不需要它。
• LTL：我不确定该属性是否符合您的想法。我会写： G ( proc != write -> (memory.K = next(memory.K)) )

如果您有此示例用另一种语言（例如 C）编码，或者您可以修改问题的描述，那么我可以为您提供更多信息。