モデル検査とSAT

Menu


モデル検査


SAT

Boolean Formula の satisfiabity を調べるツール

時間は入ってない

cryptominisat


Spin

Spin Promela という言語で仕様を記述するモデル検査

比較的大きな仕様まで検証できる


JavaPathfinder

Javaのモデル検査器。Thread を見てくれる。

JavaPathFinder


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文字程度で考察せよ。

例題


Shinji KONO / Wed Jan 24 15:16:18 2024