-title: モデル検査とSAT
--モデル検査
--SAT
Boolean Formula の satisfiabity を調べるツール
時間は入ってない
cryptominisat
--Spin
Spin
Promela という言語で仕様を記述するモデル検査
比較的大きな仕様まで検証できる
--JavaPathfinder
Javaのモデル検査器。Thread を見てくれる。
--CPAcheker
Cで書いたプログラムを検証してくれる
CPachecker
--mCRL2
独自言語
mCRL2
--PRISM
確率付きオートマトン
PRISM
--TLA+
TLA+
--nuXmv
nuXmv
tutorial
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
--その他の例題
http://nusmv.fbk.eu/examples/examples.html
---問題13.1
Turing machine の停止性のように、プログラムの正しさは原理的に証明することはできない。
それにも関わらずシステムの信頼性を高めるにはどうすれば良いか? 定理証明やモデル検査器
に触れつつ800文字程度で考察せよ。
例題