Mercurial > hg > Papers > 2021 > anatofuz-master
diff paper/chapter/01-introduction.tex @ 55:76eee6847726
...
| author | anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 02 Feb 2021 12:23:46 +0900 |
| parents | 66b32f3ec7fa |
| children | 3a8c21a37bf1 |
line wrap: on
line diff
--- a/paper/chapter/01-introduction.tex Mon Feb 01 21:44:30 2021 +0900 +++ b/paper/chapter/01-introduction.tex Tue Feb 02 12:23:46 2021 +0900 @@ -30,7 +30,7 @@ 他の形式手法にモデル検査がある。 -モデル検査は実際に動作するコードですべての可能な実行の組み合わせを実行し検証する方法である。 +モデル検査はプログラムの可能な実行をすべて数え上げて要求している使用を満たしているかどうかを調べる手法である。 例えばJavaのソースコードに対してモデル検査をするJavaPathFinderなどがある。 モデル検査を利用する場合は、実際に動作するコード上で検証を行うことが出来る。 OSのソースコードそのものをモデル検査すると、実際に検証されたOSが動作可能となる。