モデル検査と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.smvtest7.smv
% nuXmv test8.smvtest8.smv
% nuXmv test9.smvtest9.smv
% nuXmv test10.smv % nuXmv -bmc -bmc_length 4 test10.smvtest10.smv