SMV 模型檢測工具的使用

前言

SMV是一個符号驗證工具，是一個特别經典的形式化驗證工具。本博文就關于如何安裝smv做一些介紹。

SMV安裝

linux 源碼安裝

wget http://www.cs.cmu.edu/~modelcheck/smv/smv.r2.5.4.tar.gz
tar -xvf smv.r.2.5.4.tar.gz
cd smv
make
           

如果報如下錯誤：

yacc找不到

則先安裝flex和bison

sudo apt-get install flex bison
           

然後再make.

如果報

y.tab.c:520:7: error: conflicting types for ‘malloc’
           

window 安裝

http://www.cs.cmu.edu/~modelcheck/smv/smv-nt2.5.zip

解壓開來即可

使用樣例

先編輯好有限狀态機來，儲存成 . s m v .smv .smv 格式結尾的檔案，然後使用svm.exe +檔案名 既可。

樣例：

examples/counter.smv

MODULE main
VAR
  bit0 : counter_cell(1);
  bit1 : counter_cell(bit0.carry_out);
  bit2 : counter_cell(bit1.carry_out);
SPEC
  AG AF bit2.carry_out

MODULE counter_cell(carry_in)
VAR
  value : boolean;
ASSIGN
  init(value) := 0;
  next(value) := value + carry_in mod 2;
DEFINE
  carry_out := value & carry_in;

           

這是一個3位的加法器。它的目标是為了檢驗看最高位是否會進位。main裡面的SEPC 指定需要檢驗的安全屬性。

運作結果：

-- specification AG AF bit2.carry_out is true

resources used:
processor time: 0.003 s,
BDD nodes allocated: 62
Bytes allocated: 1045232
BDD nodes representing transition relation: 14 + 1
           

使用方法

SMV的核心是在ASSIGN裡面定義好有限狀态機之間的狀态轉移，然後在SEPC裡面使用CTL 計算樹邏輯表示出所要檢驗的性質。如果狀态機滿足相應的性質，那麼它就顯示對應的sepecification為true，否則就給出一條路徑證明這個sepecification是錯誤的。

說明文檔

https://download.csdn.net/download/jmh1996/10886833

一個小trick

因為smv隻輸出不滿足性質的路徑，是以如果我們想找出滿足原性質的路徑，隻需要寫目标形式的非即可。

例如上面的例子：

AG AF bit2.carry_out
           

表示所需檢驗的性質是對于所有的路徑，這些路徑都存在某個節點使用bit2.carry_out為1.

那麼它的非就是 所有路徑的bit2.carry_out全部為0.

AG bit2.carry_out=0
           

然後跑一波即可。