NuSMV

4日で学ぶモデル検査 初級編
https://www.amazon.co.jp/dp/4860431197/
519WB8K75ML._SX352_BO1,204,203,200_.jpg

モデル検査 初級編―基礎から実践まで4日で学べる (CVS教程)
https://www.amazon.co.jp/dp/4764955059/
41IXKItcipL._SX348_BO1,204,203,200_.jpg

NuSMVとSPINで記述している。

導入

http://nusmv.fbk.eu/

Getting the NuSMV Source Code
http://nusmv.fbk.eu/NuSMV/download/getting_src-v2.html

Getting the NuSMV Binary Code
http://nusmv.fbk.eu/NuSMV/download/getting_bin-v2.html

5種類あります。
GNU/Linux libc6 (686) 32-bit

GNU/Linux libc6 (x86) 64-bit

MacOSX Darwin (x86) 64-bit

Windows archive 32-bit (586)

Windows archive 64-bit (x86)

With ZCHAFFとwithout ZCHAFFが選べます。

 ZCHAFF is for non-commercial purposes only. 
NO COMMERCIAL USE OF ZCHAFF IS ALLOWED WITHOUT WRITTEN PERMISSION FROM PRINCETON UNIVERSITY. 
Please contact Sharad Malik (malik@ee.princeton.edu) for details. |

sample

systemalpha.smv
MODULE main

VAR
a:{0,1,2};
b:{0,1,2};
sw:{on, off};

ASSIGN
 init(a) := 0;
 next(a) := case
    b = 1:a;
    1:(a+1) mod 3;
    esac;

init(b) := 0;
next(b) := case
    a = b:b;
    1 :(b+1) mod 3;

init(sw) : = off;
    a=2 & b = 2: on;
    a=1 & b = 1: off;
    1 :sw;
    esac;

LTLSPEC G ( sw = off -> F (sw = on))
LTLSPEC G ( sw = on -> F (sw = off))

実行結果

$ ./NuSMV systemalpha.smv 
*** This is NuSMV 2.6.0 (compiled on Wed Oct 14 15:31:33 2015)
*** Enabled addons are: compass
*** For more information on NuSMV see <http://nusmv.fbk.eu>
*** or email to <nusmv-users@list.fbk.eu>.
*** Please report bugs to <Please report bugs to <nusmv-users@fbk.eu>>

*** Copyright (c) 2010-2014, Fondazione Bruno Kessler

*** This version of NuSMV is linked to the CUDD library version 2.4.1
*** Copyright (c) 1995-2004, Regents of the University of Colorado

*** This version of NuSMV is linked to the MiniSat SAT solver. 
*** See http://minisat.se/MiniSat.html
*** Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
*** Copyright (c) 2007-2010, Niklas Sorensson

WARNING *** This version of NuSMV is linked to the zchaff SAT         ***
WARNING *** solver (see http://www.princeton.edu/~chaff/zchaff.html). ***
WARNING *** Zchaff is used in Bounded Model Checking when the         ***
WARNING *** system variable "sat_solver" is set to "zchaff".          ***
WARNING *** Notice that zchaff is for non-commercial purposes only.   ***
WARNING *** NO COMMERCIAL USE OF ZCHAFF IS ALLOWED WITHOUT WRITTEN    ***
WARNING *** PERMISSION FROM PRINCETON UNIVERSITY.                     ***
WARNING *** Please contact Sharad Malik (malik@ee.princeton.edu)      ***
WARNING *** for details.                                              ***


file systemalpha.smv: line 20: at token "init": syntax error


file systemalpha.smv: line 20: Parser error

NuSMV terminated by a signal

Aborting batch mode
systemalpha.smv
MODULE main

VAR
a:{0,1,2};
b:{0,1,2};
sw:{on, off};

ASSIGN
 init(a) := 0;
 next(a) := case
    b = 1:a;
    1:(a+1) mod 3;
    esac;

init(b) := 0;
next(b) := case
    a = b:b;
    1 :(b+1) mod 3;
    esac;

init(sw) : = off;
    a=2 & b = 2: on;
    a=1 & b = 1: off;
    1 :sw;
    esac;

LTLSPEC G ( sw = off -> F (sw = on))
LTLSPEC G ( sw = on -> F (sw = off))
file systemalpha.smv: line 21: at token ":": syntax error


file systemalpha.smv: line 21: Parser error

NuSMV terminated by a signal

Aborting batch mode
init(sw) := off;

空白を詰めた。

file systemalpha.smv: line 22: at token "=": syntax error
file systemalpha.smv: line 22: Parser error

NuSMV terminated by a signal

Aborting batch mode
next(sw) := case

追加

TYPE ERROR file systemalpha.smv: line 12 : illegal left operand type of ":". It should be boolean, but is integer

TYPE ERROR file systemalpha.smv: line 18 : illegal left operand type of ":". It should be boolean, but is integer

TYPE ERROR file systemalpha.smv: line 25 : illegal left operand type of ":". It should be boolean, but is integer

file systemalpha.smv: Type System Violation detected


Aborting batch mode

NuSMV terminated by a signal

Aborting batch mode

TYPE ERROR file systemalpha.smv: line 12 : illegal left operand type of ":". It should be boolean, but is integer

TYPE ERROR file systemalpha.smv: line 18 : illegal left operand type of ":". It should be boolean, but is integer

TYPE ERROR file systemalpha.smv: line 25 : illegal left operand type of ":". It should be boolean, but is integer

file systemalpha.smv: Type System Violation detected


Aborting batch mode

NuSMV terminated by a signal

Aborting batch mode

Qiita on NuSMV

NuSMVでコンセンサスアルゴリズム (の超一部) をモデル検査する
https://qiita.com/shinsa82/items/c66b91047c2174929ae1

NuSMVによるモデル検査入門 (1) ステートマシンを定義する
https://qiita.com/shinsa82/items/cd4d95c616bf1da852ce

参考文献

モデル検査ツールについて
Copyright© FormalTech Co., Ltd. all rights reserved.
株式会社フォーマルテック
http://www.formaltech.co.jp/aboutMCtool.pdf

NuSMV を用いた CTL*のモデル検査器の実装
東京工業大学 理学部 情報科学科藤原一貴(0521236)
平成 20 年度卒業論文
指導教官 佐々 政孝 教授 2009年2月5日
http://www.is.titech.ac.jp/~sassa/lab/papers-written/05B21236-fujiwara.pdf

モデル検査ツール NuSMV を用いたオントロジー検証 Ontology Verification using the Model Checker NuSMV, 阿部 雄貴
http://oberon.nagaokaut.ac.jp/katsuk/papers/fit/11/data/pdf/B-005.pdf

NuSMVによるモデリング.
http://lis2.huie.hokudai.ac.jp/~kurihara/classes/Program/nusmvspin.ppt