４日で学ぶモデル検査 初級編
https://www.amazon.co.jp/dp/4860431197/
モデル検査 初級編―基礎から実践まで4日で学べる (CVS教程)
https://www.amazon.co.jp/dp/4764955059/
NuSMVとSPINで記述している。
導入
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
５種類あります。
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
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
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
＜この記事は個人の過去の経験に基づく個人の感想です。現在所属する組織、業務とは関係がありません。＞
This article is an individual impression based on the individual's experience. It has nothing to do with the organization or business to which I currently belong.
文書履歴(document history)
ver. 0.01 初稿 20180318
ver. 0.04 URL追記 20230226
最後までおよみいただきありがとうございました。
いいね 💚、フォローをお願いします。
Thank you very much for reading to the last sentence.
Please press the like icon 💚 and follow me for your happy life.