モデル検査とSAT
Menu
モデル検査
SAT
Boolean Formula の satisfiabity を調べるツール時間は入ってない
Spin
Spin Promela という言語で仕様を記述するモデル検査比較的大きな仕様まで検証できる
JavaPathfinder
Javaのモデル検査器。Thread を見てくれる。CPAcheker
Cで書いたプログラムを検証してくれるmCRL2
独自言語PRISM
確率付きオートマトンTLA+
TLA+nuXmv
nuXmvtutorial
a か b のどちらかを非決定的に取る automaton を考える。
MODULE main
VAR
state : {a, b};
ASSIGN
init(state) := a;
next(state) := {a, b};
状態 a から始まって、任意のaとb の木構造な可能な実行がある。
それぞれの可能な実行を path という。
CTL
A はすべてのpath、E はあるpath について成り立つ。G はすべての時間(□)、F はいつか(<>)。これの組み合わせになる。
a U b は、b になるまでずーっとa 。b になる必要はある。
SPEC AG state=a
SPEC EG state=a
SPEC AF state=a
SPEC EF state=a
SPEC A [ state=a U state=b ]
SPEC E [ state=a U state=b ]
LTL
一つの時間軸についてだけの様相論理。
G はすべての時間(□)、F はいつか(<>)。これの組み合わせになる。
a U b は、b になるまでずーっとa 。b になる必要はある。
nuXmv は false になる可能性を調べる。
LTLSPEC G state=a
LTLSPEC F state=a
LTLSPEC G [ state=a U state=b ]
LTLSPEC F [ state=a U state=b ]
smv example
このセマフォは、critical にずーっと入れるので成り立たない性質がある。
% nuXmv -int test7.smv
test7.smv
% nuXmv test8.smv
test8.smv
% nuXmv test9.smv
test9.smv
% nuXmv test10.smv
% nuXmv -bmc -bmc_length 4 test10.smv
test10.smv