--- a/paper/text/introduction.tex	Sat Jan 22 15:00:30 2022 +0900
+++ b/paper/text/introduction.tex	Sat Jan 29 20:27:16 2022 +0900
@@ -1,10 +1,23 @@
-\chapter{序論}
-本章は，標準として「背景と目的」および「論文の構成」の2節で構成される．分量の規定はないが，2節合わせて2$\sim $3ページ程度が標準的である．
+\chapter{GearsOSにおけるデバッグ}
+
+OSはCPUの割り当てやスケジュール、記憶容量へのアクセスなどアプリケーションが動作する上で土台となる重要なソフトウェアである。
+そのためOSの信頼性は高く保証されている必要がある。
+信頼性を保証する方法として形式検証が挙げられる。
+形式検証には定理証明とモデル検査があり、定理証明はAgda\cite{agda}などの定理証明支援系を用いて数学的にプログラムの信頼性を保証する。
+モデル検査はプログラムが特定の状態から遷移しうる全ての状態を数え上げ、
+仕様を満たしているかどうかを検査することでプログラムの信頼性を保証する。
 
-\section{背景と目的}
-この節には，研究の背景と目的を記述する．研究の社会的もしくは学術的な意義を明らかにするものとする．
+本研究室では定理証明やモデル検査を用いて信頼性の保証を行うGearsOSの開発を行っている。
+GearsOSはContinuation Based C(CbC)を用いて記述したOSで、CbCは本研究室で開発している言語で、CodeGearというプログラム単位で記述・遷移するC言語の下位言語である。
+CodeGear間の遷移は通常の関数呼び出しではなく、goto文によって行われるため、呼び出し元へ戻らない。
+そのためプログラムの記述をそのまま状態遷移として落とし込むことができ、これにより定理証明やモデル検査が可能である。
 
-\section{論文の構成}
-この節では，卒業論文の全体構成を述べる．論文の構成は研究分野によって異なるので，指導教員と調整すると良い．その上で，卒業論文の内容に従って以下の例のように論文の構成を記述しなさい．この記述形式でないといけないということではないので，各自で適切に調整しなさい．
+GearsOSは定理証明やモデル検査により信頼性の保証を行っているが、
+これらの定理証明やモデル検査自体を自分がどう証明したのかを確かめたり、GearsOS上の例題のデバッグしたいということがある。
+現状このような場合にはGDB\cite{gdb}やLLDB\cite{lldb}などの既存のデバッガを用いて変数の値の確認や、
+スタックトレースによる関数呼び出しの確認を行うことでデバッグを行っている。
+しかし、GearsOSは変数の格納方法が複雑なため煩雑な記述を行わなければならない特性や、
+スタックを持たないためにスタックトレースが使えないなどの特性を持つ。これらの特性によりプログラムの遷移の流れや、
+変数の値の変化など既存デバッガを用いたデバッグが難しいという問題がある。
 
-本論文は以下の章で構成される．第1章の○○(○○に章タイトルを記述する)に続き，第2章の関連研究では△△△について述べる．第3章では，□□□について本論文で新たに提案する手法について述べる．第4章では，提案手法での植物形態の三次元再構成精度検証実験について述べるとともに，既存の研究結果との比較考察を述べる．最後に，第5章で本論文のまとめと今後の展望について述べる．
+本研究ではGearsOS特化のデバッガを開発することでエラー・バグの発見および修正のコストを下げるとともにさらなるGearsOSの信頼性の向上を目指す。