Binary file Paper/sigos.pdf has changed

--- a/Paper/sigos.tex	Tue May 07 21:16:04 2019 +0900
+++ b/Paper/sigos.tex	Tue May 07 22:00:58 2019 +0900
@@ -58,9 +58,8 @@
 
 \maketitle
 
-\section{OS の評価の容易化}
-OS はさまざまなコンピュータの信頼性の基本である。OS の信頼性を保証する事自体が難しいが、時代とともに進歩するハードウェア、サービスに対応して OS 自体が拡張される必要がある。さらに非決定的な実行を持つ為、モデル検査は無限の状態ではなくても巨大な状態を調べることになり、状態を有限に制限したり状態を抽象化したりする方法が用いられている。現段階で動作する OS として xv6 を採用し、 CbCで書き換えることにより stackを排除し状態遷移化することができる。状態遷移化することにより状態を有限化させることが可能となるため、評価が容易になる。よって評価を容易にするためにxv6 kernel をCbC で書き換え状態遷移に落とし込むことを目的とする。
-
+\section{はじめに}
+OS はさまざまなコンピュータの信頼性の基本である。OS の信頼性を保証する事自体が難しいが、時代とともに進歩するハードウェア、サービスに対応して OS 自体が拡張される必要がある。さらに非決定的な実行を持つ為、モデル検査は無限の状態ではなくても巨大な状態を調べることになり、状態を有限に制限したり状態を抽象化したりする方法が用いられている。 xv6 はシンプルで扱いやすい基本的な構造を持つ OSである。このxv6 から Stack を排除することで OS の状態を有限化させることが可能となる。当研究室で開発している Continuation based C を用いてxv6 kernel を書き換えることでOSの状態を有限化可能であるかを検討する。
 
 \section{Continuation based C}
 \subsection{CbCの概要}