|
127
|
1 -title: モデル検査とSAT
|
|
|
2
|
|
|
3 --モデル検査
|
|
|
4
|
|
|
5 --SAT
|
|
|
6
|
|
164
|
7 Boolean Formula の satisfiabity を調べるツール
|
|
|
8
|
|
|
9 時間は入ってない
|
|
|
10
|
|
|
11 <a href="https://github.com/msoos/cryptominisat"> cryptominisat </a>
|
|
|
12
|
|
|
13 --Spin
|
|
|
14
|
|
|
15 <a href="https://github.com/nimble-code/Spin"> Spin </a>
|
|
|
16
|
|
|
17 Promela という言語で仕様を記述するモデル検査
|
|
|
18
|
|
|
19 比較的大きな仕様まで検証できる
|
|
|
20
|
|
|
21 --JavaPathfinder
|
|
|
22
|
|
|
23 Javaのモデル検査器。Thread を見てくれる。
|
|
|
24
|
|
|
25 --CPAcheker
|
|
|
26
|
|
|
27 Cで書いたプログラムを検証してくれる
|
|
|
28
|
|
|
29 <a href="https://cpachecker.sosy-lab.org/doc.php"> CPachecker</a>
|
|
|
30
|
|
|
31 --mCRL2
|
|
|
32
|
|
|
33 独自言語
|
|
|
34
|
|
|
35 <a href="https://www.mcrl2.org/web/user_manual/index.html"> mCRL2 </a>
|
|
|
36
|
|
|
37 --PRISM
|
|
|
38
|
|
|
39 確率付きオートマトン
|
|
|
40
|
|
|
41 <a href="http://www.prismmodelchecker.org/people.php"> PRISM </a>
|
|
|
42
|
|
|
43 --TLA+
|
|
|
44
|
|
|
45 <a href="http://lamport.azurewebsites.net/tla/toolbox.html"> TLA+ </a>
|
|
|
46
|
|
127
|
47 --nuXmv
|
|
|
48
|
|
|
49 <a href="https://nuxmv.fbk.eu">nuXmv </a> <br>
|
|
|
50
|
|
|
51 <a href="http://nusmv.fbk.eu/NuSMV/tutorial/index.html"> tutorial </a> <br>
|
|
|
52
|
|
|
53 a か b のどちらかを非決定的に取る automaton を考える。
|
|
|
54
|
|
|
55 MODULE main
|
|
|
56 VAR
|
|
|
57 state : {a, b};
|
|
|
58 ASSIGN
|
|
|
59 init(state) := a;
|
|
|
60 next(state) := {a, b};
|
|
|
61
|
|
|
62 状態 a から始まって、任意のaとb の木構造な可能な実行がある。
|
|
|
63
|
|
|
64 それぞれの可能な実行を path という。
|
|
|
65
|
|
|
66 --CTL
|
|
|
67
|
|
|
68 A はすべてのpath、E はあるpath について成り立つ。
|
|
|
69
|
|
|
70 G はすべての時間(□)、F はいつか(<>)。これの組み合わせになる。
|
|
|
71
|
|
|
72 a U b は、b になるまでずーっとa 。b になる必要はある。
|
|
|
73
|
|
|
74 SPEC AG state=a
|
|
|
75 SPEC EG state=a
|
|
|
76 SPEC AF state=a
|
|
|
77 SPEC EF state=a
|
|
|
78 SPEC A [ state=a U state=b ]
|
|
|
79 SPEC E [ state=a U state=b ]
|
|
|
80
|
|
|
81 --LTL
|
|
|
82
|
|
|
83 一つの時間軸についてだけの様相論理。
|
|
|
84
|
|
|
85 G はすべての時間(□)、F はいつか(<>)。これの組み合わせになる。
|
|
|
86
|
|
|
87 a U b は、b になるまでずーっとa 。b になる必要はある。
|
|
|
88
|
|
|
89 nuXmv は false になる可能性を調べる。
|
|
|
90
|
|
|
91 LTLSPEC G state=a
|
|
|
92 LTLSPEC F state=a
|
|
|
93 LTLSPEC G [ state=a U state=b ]
|
|
|
94 LTLSPEC F [ state=a U state=b ]
|
|
|
95
|
|
|
96 --smv example
|
|
|
97
|
|
|
98 <center><img src="fig/semaphore.svg"></center>
|
|
|
99
|
|
|
100 このセマフォは、critical にずーっと入れるので成り立たない性質がある。
|
|
|
101
|
|
|
102
|
|
|
103 % nuXmv -int test7.smv
|
|
|
104
|
|
|
105 <a href="smv/test7.smv"> test7.smv </a>
|
|
|
106
|
|
|
107 % nuXmv test8.smv
|
|
|
108
|
|
|
109 <a href="smv/test8.smv"> test8.smv </a>
|
|
|
110
|
|
|
111 % nuXmv test9.smv
|
|
|
112
|
|
|
113 <a href="smv/test9.smv"> test9.smv </a>
|
|
|
114
|
|
|
115 % nuXmv test10.smv
|
|
|
116
|
|
|
117 % nuXmv -bmc -bmc_length 4 test10.smv
|
|
|
118
|
|
|
119 <a href="smv/test10.smv"> test10.smv </a>
|
|
|
120
|
|
|
121 --その他の例題
|
|
|
122
|
|
|
123 <a href="http://nusmv.fbk.eu/examples/examples.html"> http://nusmv.fbk.eu/examples/examples.html
|
|
|
124
|
|
|
125 ---問題13.1
|
|
|
126
|
|
|
127 Turing machine の停止性のように、プログラムの正しさは原理的に証明することはできない。
|
|
|
128 それにも関わらずシステムの信頼性を高めるにはどうすれば良いか? 定理証明やモデル検査器
|
|
|
129 に触れつつ800文字程度で考察せよ。
|
|
|
130
|
|
|
131 <a href=""> 例題 </a> <!--- Exercise 13.1 --->
|
|
|
132
|
|
|
133
|
|
|
134
|
|
|
135
|
