使用NuSMV進行模型檢查

Question

確實在NuSMV中沒有像NULL，Nil，None這樣的值嗎？

而且我們不應該爲過程建立模型，因爲模型應該重複電子電路？

我的方案是我有一個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中沒有像NULL，無，無值？

從同樣的意義上說，它對於C而言是正確的。Nil只是給定數據類型所允許值的一個值。看看你的例子，似乎你真的不需要它，不是嗎？

而且我們不應該爲過程建立模型，因爲模型應該代表電子電路？

不可以。只要您不需要創建動態對象（例如C中的malloc），就可以表示任何您想要的內容。另一個問題是關於進程的同步性/併發性。您仍然可以建模異步進程，但它需要明確編碼調度程序。

關於代碼：我沒有運行它，但很多事情看起來很可疑。我建議您嘗試使用NuSMV模擬命令來查看模型的行爲。

• UART模塊：您只寫入Rx和Tx。這些值永遠不會被讀取。
• UART模塊：我建議不要混合ASSIGN和TRANS。這是一種在模型中引入死鎖的簡單方法。而且，你寫的TRANS已經包含在ASSIGN中了。
• UART模塊：你爲什麼需要狀態變量？
• MEM模塊：我不明白你爲什麼使用數組，因爲你只看到兩個值。我認爲你可以更多地抽象出這個部分。從你的非正式描述看來，你似乎不需要它。
• LTL：我不確定房產是否能夠捕捉到您的想法。我會寫：G（proc！= write - >（memory.K = next（memory.K）））

如果你有用另一種語言編碼的例子（例如C），或者你可以修改問題描述，然後我可以爲您提供更多信息。