Mercurial > hg > Papers > 2021 > anatofuz-master

comparison paper/chapter/01-introduction.tex @ 55:76eee6847726

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
date Tue, 02 Feb 2021 12:23:46 +0900
parents 66b32f3ec7fa
children 3a8c21a37bf1
comparison
equal deleted inserted replaced
54:2cbaf041b085 55:76eee6847726
28 検証されたアルゴリズムをもとにCで実装することは可能であるが、 この場合移植時にバグが入る可能性がある。 28 検証されたアルゴリズムをもとにCで実装することは可能であるが、 この場合移植時にバグが入る可能性がある。
29 検証ができているソースコードそのものを使ってOSを動作させたい。 29 検証ができているソースコードそのものを使ってOSを動作させたい。
30 30
31 31
32 他の形式手法にモデル検査がある。 32 他の形式手法にモデル検査がある。
33 モデル検査は実際に動作するコードですべての可能な実行の組み合わせを実行し検証する方法である。 33 モデル検査はプログラムの可能な実行をすべて数え上げて要求している使用を満たしているかどうかを調べる手法である。
34 例えばJavaのソースコードに対してモデル検査をするJavaPathFinderなどがある。 34 例えばJavaのソースコードに対してモデル検査をするJavaPathFinderなどがある。
35 モデル検査を利用する場合は、実際に動作するコード上で検証を行うことが出来る。 35 モデル検査を利用する場合は、実際に動作するコード上で検証を行うことが出来る。
36 OSのソースコードそのものをモデル検査すると、実際に検証されたOSが動作可能となる。 36 OSのソースコードそのものをモデル検査すると、実際に検証されたOSが動作可能となる。
37 しかしOSの処理は膨大である。 37 しかしOSの処理は膨大である。
38 すべての存在可能な状態を数え上げるモデル検査では状態爆発が問題となる。 38 すべての存在可能な状態を数え上げるモデル検査では状態爆発が問題となる。