--- a/paper/chapter/02-perl.tex	Sat Jan 30 22:42:58 2021 +0900
+++ b/paper/chapter/02-perl.tex	Sun Jan 31 11:36:32 2021 +0900
@@ -26,7 +26,7 @@
 その為GearsOSの拡張部分を、等価な純粋なCbCの記述に変換する必要がある。
 現在のGearsOSでは、 CMakeによるコンパイル時にPerlで記述された\texttt{generate\_stub.pl}と\texttt{generate\_context.pl}の2種類のスクリプトで変換される。
 
- 
+
 
 \begin{itemize}
   \item \texttt{generate\_stub.pl}
@@ -66,7 +66,7 @@
 GCCの場合は最初からターゲットアーキテクチャを指定してコンパイラをビルドする必要がある。
 
 時にマシンスペックの問題などから、 別のアーキテクチャ向けのバイナリを生成したいケースがある。
-教育用マイコンボードであるRaspberry PiはARMアーキテクチャが搭載されている。
+教育用マイコンボードであるRaspberry Pi\cite{rpi}はARMアーキテクチャが搭載されている。
 Raspberry Pi上でGearsOSのビルドをする場合、 ARM用にビルドされたCbCコンパイラが必要となる。
 Raspberry Pi自体は非力なマシンであるため、 GearsOSのビルドはもとよりCbCコンパイラの構築をRaspberry Pi上でするのは困難である。
 マシンスペックが高めのx86マシンからARM用のバイナリをビルドして、 Raspberry Piに転送し実行したい。
@@ -98,7 +98,7 @@
   \caption{pmake.plの処理フロー}
   \label{fig:pmake}
  \end{figure}
- 
+
 
 
 \section{GearsCbCのInterfaceの実装時の問題}

--- a/paper/chapter/introduction.tex	Sat Jan 30 22:42:58 2021 +0900
+++ b/paper/chapter/introduction.tex	Sun Jan 31 11:36:32 2021 +0900
@@ -5,12 +5,8 @@
 信頼性の保証には、 実行してほしい一連の挙動をまとめた仕様と、 それを満たしているかどうかの確認である検証が必要となる。
 アプリケーション開発では検証に関数や一連の動作をテストを行う方法や、デバッグを通して信頼性を保証する手法が広く使われている。
 
-アプリケーションは通常特定のプログラミング言語で実装されている。
-このプログラミング言語自身の信頼性は高く保証される必要がある。
-また、実際にアプリケーションを動作させるOSも高い信頼性が保証される必要がある。
+実際にアプリケーションを動作させるOSは、アプリケーションよりさらに高い信頼性が保証される必要がある。
 OSはCPUやメモリなどの資源管理と、 ユーザーにシステムコールなどのAPIを提供することで抽象化を行っている。
-
-
 OSの信頼性の保証もテストコードを用いて証明することも可能ではあるが、 アプリケーションと比較するとOSのコード量、 処理の量は膨大である。
 またOSはCPU制御やメモリ制御、 並列・並行処理などを多用する。
 テストコードを用いて処理を検証する場合、テストコードとして特定の状況を作成する必要がある。
@@ -19,8 +15,8 @@
 
 
 テストコード以外の方法として、 形式手法的と呼ばれるアプローチがある。
-形式手法の具体的な検証方法の中で、 証明を用いる方法とモデル検査を用いる方法がある。
-証明を用いる方法ではAgdaやCoqなどの定理証明支援系を利用し、 数式的にアルゴリズムを記述する。
+形式手法の具体的な検証方法の中で、 証明を用いる方法\cite{Yang:2010:SLI:1806596.1806610}\cite{Klein:2009:SFV:1629575.1629596}\cite{Sigurbjarnarson:2016:PVF:3026877.3026879}\cite{Chen:2015:UCH:2815400.2815402}とモデル検査を用いる方法がある。
+証明を用いる方法ではAgda\cite{agda}やCoqなどの定理証明支援系を利用し、 数式的にアルゴリズムを記述する。
 Curry-Howard同型対応則により、型と論理式の命題が対応する。
 この型を導出するプログラムと実際の証明が対応する。
 特定の型を入力として受け取り、証明したい型を生成する関数を作成する。
@@ -46,7 +42,7 @@
 その処理に着目するとOSは様々な状態を遷移して処理を行っていると考えることができる。
 OSを巨大な状態遷移マシンと考えると、 OSの処理の特定の状態の遷移まで範囲を絞ることができる。
 範囲が限られているため、有限時間でモデル検査などで検証することが可能である。
-この為にはOSの処理を状態遷移系で表現し、 証明しやすくする必要がある。
+この為にはOSの処理を状態遷移系で表現し、 証明しやすくする必要がある。\cite{hyperkernel}
 
 
 証明を行う対象の計算は、 その意味が大きく別けられる。

Binary file paper/master_paper.pdf has changed

--- a/paper/reference.bib	Sat Jan 30 22:42:58 2021 +0900
+++ b/paper/reference.bib	Sun Jan 31 11:36:32 2021 +0900
@@ -113,8 +113,8 @@
 
 @article{
     agda-ryokka,
-    author = "Hokama MASATAKA and Shinji KONO",
-    title = "GearsOS の Hoare Logic をベースにした検証手法",
+    author = "外間政尊 and 河野真治",
+    title = "GearsOS の Hoare Logic をべースにした検証手法",
     journal = "ソフトウェアサイエンス研究会",
     month = "Jan",
     year = 2019
@@ -177,7 +177,7 @@
 @article{
     gears,
     author = "河野 真治 and 伊波 立樹 and  東恩納 琢偉",
-    title = "Code Gear、Data Gear に基づく OS のプロトタイプ",
+    title = "Code Gear、Data Gear に基づく OS のプロトタイプ",
     journal = "情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)",
     month = "May",
     year = 2016