基于NuSMV的模型检验

Question

在NuSMV中没有空值、零值、无值，这是真的吗？

我们不应该为一个过程做一个模型，因为这些模型应该修复电子电路？

我的场景是，我有一个UART连接器、一个主内存和一个进程，后者在其中读写主存，并将其读写到UART。在主内存中，有名为K的数据应该保持不变。我们希望证明，如果进程没有写入K' then the value of，则K`等于它的下一个值。

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

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中没有空值、零值、无值，这是真的吗？

同样意义上也是如此，对于C. Nil只是给定数据类型所允许的值中的一个值。看看你的例子，似乎你其实并不需要它，不是吗？

我们不应该为一个过程做一个模型，因为模型应该代表电子电路？

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

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

• UART模块:您只写到Rx和Tx。这些价值永远不会被读取。
• UART模块:我建议不要混合分配和转换。这是在模型中引入死锁的简单方法。此外，您编写的反式已经包含在赋值中。
• UART模块:为什么需要状态变量？
• MEM模块:我不明白你为什么要使用数组，因为你只看两个值。我想你可以把这部分更抽象一些。从你的非正式描述来看，你似乎不需要它。
• LTL:我不确定这个财产是否符合你的想法。我会写:G( proc !=写-> (Memy.K=next(Memy.K)

如果您用另一种语言(例如，C)编码了这个示例，或者您可以修改问题的描述，那么我可以向您提供更多的信息。