# HG changeset patch
# User anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
# Date 1611834428 -32400
# Node ID 36d24119450791e5e3c7c95ebaa16c0cdd44b355
# Parent  7c6d3d582554be1987354009e0de7cc940cd2bc9
...

diff -r 7c6d3d582554 -r 36d241194507 paper/chapter/introduction.tex
--- a/paper/chapter/introduction.tex	Thu Jan 28 13:58:12 2021 +0900
+++ b/paper/chapter/introduction.tex	Thu Jan 28 20:47:08 2021 +0900
@@ -17,7 +17,23 @@
 実際にOSが動作する中でバグやエラーを発生する条件を、 並列処理の状況などを踏まえてテストコードで表現するのは困難である。
 非決定的な処理を持つOSの信頼性を保証するには、 テストコード以外の手法を用いる必要がある。
 
+
 テストコード以外の方法として、 形式手法的と呼ばれるアプローチがある。
 形式手法の具体的な検証方法の中で、 証明を用いる方法とモデル検査を用いる方法がある。
 証明を用いる方法ではAgdaやCoqなどの定理証明支援系を利用し、 数式的にアルゴリズムを記述する。
-Curry-Howard同型対応則により、型と命題が、 プログラムと証明が対応する。
+Curry-Howard同型対応則により、型と論理式の命題が対応する。
+この型を導出するプログラムと実際の証明が対応する。
+特定の型を入力として受け取り、証明したい型を生成する関数を作成する。
+証明そのものは記述した関数の内容の整合性を、定理証明支援系が検証する。
+証明を使う手法の場合、 実際の証明を行うのは定理証明支援系であるため、 定理証明支援系が理解できるプログラムで実装する必要がある。
+AgdaやCoqの場合はAgda、 Cow自身のプログラムで記述する必要がある。
+しかしAgdaで証明ができてもAgdaのコードを直接OSのソースコードとしてコンパイルすることはできない。
+Agda側でCのソースコードを吐き出せれば可能ではあるが、 現状は検証したコードと実際に動作するコードは分離されている。
+検証ができているソースコードそのものを使ってOSを動作させたい。
+
+
+他の形式手法にモデル検査がある。
+モデル検査は実際に動作するコードですべての可能な実行の組み合わせを実行し検証する方法である。
+モデル検査を利用する場合は、実際に動作するコード上で検証を行うことが出来る。
+実装するコードに対してモデル検査を行いたいが、モデル検査を行うモデル検査器は限られている。
+例えばJavaのソースコードに対してモデル検査をするJavaPathFinderなどがある。
diff -r 7c6d3d582554 -r 36d241194507 paper/master_paper.pdf
Binary file paper/master_paper.pdf has changed