--- 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が動作可能となる。

--- a/paper/chapter/02-cbc.tex	Mon Feb 01 21:44:30 2021 +0900
+++ b/paper/chapter/02-cbc.tex	Tue Feb 02 12:23:46 2021 +0900
@@ -7,6 +7,7 @@
 Agda よる関数型のCbCの記述も用意されている。
 実際のOSやアプリケーションを記述する場合には、GCC及びLLVM/clang上のCbC実装を用いる。
 
+
 \section{CodeGear}
 CbCでは関数の代わりにCodeGearという単位でプログラミングを行う。
 CodeGearは通常のCの関数宣言の返り値の型の代わりに\texttt{\_\_code}で宣言を行う。
@@ -14,8 +15,6 @@
 入力のDataGearをInputDataGearと呼び、 出力のDataGearをOutputDataGearと呼ぶ。
 CodeGearがアクセスできるDataGearは、 InputDataGearとOutputDataGearに限定される。
 
-
-
 CodeGearは関数呼び出し時のスタックを持たない為、一度あるCodeGearに遷移してしまうと元の処理に戻ってくることができない。
 しかしCodeGearを呼び出す直前のスタックは保存される。
 部分的にCbCを適用する場合はCodeGearを呼び出す\texttt{void}型などの関数を経由することで呼び出しが可能となる。
@@ -26,7 +25,12 @@
 LLVM/clangでは\texttt{setjmp}と\texttt{longjmp}を使い実装している。
 したがってプログラマから見ると、通常のCの関数呼び出しの返り値をCodeGearから取得する事が可能となる。
 
-\section{DataGear}
+\section{DataGearとMetaDataGear}
+DataGearはCbCでのデータの単位である。
+基本はC言語の構造体そのものであるが、 DataGearの場合はデータに付随するメタ情報も取り扱う。
+これはデータ自身がどういう型を持っているかなどの情報である。
+ほかに計算を実行するCPU、 GPUの情報や、 計算に必要なすべてのDataGearの管理などの実行環境のメタデータもDataGearの形で表現される。
+このメタデータを扱うDataGearをMetaDataGearと呼ぶ。
 
 
 \section{CbCを使ったシステムコールディスパッチの例題}
@@ -47,8 +51,12 @@
 現在のGearsOSは並列フレームワークとして実装されており、 実用的なOSのプロトタイプ実装として既存のOS上への実装を目指している。
 
 \section{メタ計算}
+プログラミング言語からメタ計算を取り扱う場合、 言語の特性に応じて様々な手法が使われてきた。
+関数型プログラミングの見方では、 メタ計算はモナドの形で表現されていた。\cite{moggi-monad}
+OSの研究ではメタ計算の記述に型付きアセンブラを用いることもある。
 
-関数型プログラミングの見方では、 メタ計算はモナドの形で表現されていた。\cite{moggi-monad}
+CbCでのメタ計算はCodeGear、 DataGearの単位がそのまま使用できる。
+メタ計算で使われるこれらの単位はそれぞれ、 MetaCodeGear、 MetaDataGearと呼ばれる。
 
 \section{MetaCodeGear}
 

--- a/paper/chapter/abstract.tex	Mon Feb 01 21:44:30 2021 +0900
+++ b/paper/chapter/abstract.tex	Tue Feb 02 12:23:46 2021 +0900
@@ -1,5 +1,19 @@
 \chapter*{要旨}
-ここに要旨を書く
+アプリケーションの信頼性を保証するには、土台となるOSの信頼性は高く保証されていなければならない。
+信頼性を保証する方法としてテストコードを使う手法が広く使われている。
+OSのソースコードは巨大であり、並列処理など実際に動かさないと発見できないバグが存在する。
+OSの機能をテストですべて検証するのは不可能である。
+
+テストに頼らず定理証明やモデル検査などの形式手法を使用して、OSの信頼性を保証したい。
+証明を利用して信頼性を保証する定理証明は、 AgdaやCoqなどの定理証明支援系を利用することになる。
+支援系を利用する場合、各支援系でOSを実装しなければならない。
+証明そのものは可能であるが、 支援系で証明されたソースコードがそのままOSとして動作する訳ではない。
+証明されたコードと、実際に動作するOSを記述するC言語などのプログラミング言語の間にはギャップが存在し、 Cでの実装時に入ってしまうバグを取り除くことはできない。
+このためには定理証明されたコードを等価なC言語などに変換する処理系が必要となる。
+
+信頼性を保証するほかの方法として、プログラムの可能な実行をすべて数え上げて仕様を満たしているかを確認するモデル検査がある。
+モデル検査は実際に動作しているプログラムに対して実行することが可能である。
+
 
 \chapter*{Abstract}
 hogefuga

Binary file paper/master_paper.pdf has changed