-title: モデル検査とSAT

--モデル検査

--SAT

--nuXmv

<a href="https://nuxmv.fbk.eu">nuXmv  </a> <br>

<a href="http://nusmv.fbk.eu/NuSMV/tutorial/index.html"> tutorial </a> <br>

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

<center><img src="fig/semaphore.svg"></center>

このセマフォは、critical にずーっと入れるので成り立たない性質がある。


    % nuXmv -int test7.smv

<a href="smv/test7.smv"> test7.smv </a>

    % nuXmv test8.smv

<a href="smv/test8.smv"> test8.smv </a>

    % nuXmv test9.smv

<a href="smv/test9.smv"> test9.smv </a>

    % nuXmv test10.smv

    % nuXmv -bmc -bmc_length 4 test10.smv

<a href="smv/test10.smv"> test10.smv </a>

--その他の例題

<a href="http://nusmv.fbk.eu/examples/examples.html"> http://nusmv.fbk.eu/examples/examples.html

---問題13.1 

Turing machine の停止性のように、プログラムの正しさは原理的に証明することはできない。
それにも関わらずシステムの信頼性を高めるにはどうすれば良いか? 定理証明やモデル検査器
に触れつつ800文字程度で考察せよ。

<a href=""> 例題  </a> <!---  Exercise 13.1 --->