Model checking with NuSMV

Question

Is it true that in NuSMV there is no value like NULL, nil, None?

And that we should not make a model for a process because the models should repesent electronic circuits?

My scenario is that I have one UART connector, a main memory and a process where the latter reads and writes to main memory and read and write to the UART. In the main memory there is data named K that should stay the same. We want to prove that if the process doesn't write to K' then the value ofK` equals its next value.

I wonder if my model is fine-grained enough or if it is too abstract. Also if I used the right data types.

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))

Marco Marco · Accepted Answer · 2017-04-10T00:32:07

In your post you touch many topics, I am not sure which is your main question.

Is it true that in NuSMV there is no value like NULL, nil, None?

It is true in the same sense that it is true for C. Nil is only one value within the values allowed by the given data-type. Looking at your example, it seems you do not really need it anyway, no?

And that we should not make a model for a process because the models should represent electronic circuits?

No. You can represent whatever you want as long as you do not need to create dynamic object (e.g., a malloc in C). A different issue is about synchronicity/concurrency of the processes. You can still model asynchronous processes, but it requires explicitly encoding a scheduler.

Regarding the code: I did not run it, but many things look suspicious. I would suggest you try to use NuSMV simulation commands to see how the model behaves.

UART Module: You are only write to both Rx and Tx. Those values are never read.
UART Module: I would suggest against mixing ASSIGN and TRANS. That is a easy way to introduce deadlocks in your model. Moreover, the TRANS that you wrote is already subsumed by the ASSIGN
UART Module: Why do you need the state variable?
MEM Module: I do not understand why you are using an array of array, since you are only looking at two values. I think you can abstract this part more. From your informal description, it seems like you do not need it.
LTL: I am not sure whether the property captures what you have in mind. I would write: G ( proc != write -> (memory.K = next(memory.K)) )

If you have this example encoded in another language (e.g., C) or you can revise the description of the problem, then I can provide you with more information.

Model checking with NuSMV

1 Answers