--- a/paper/chapter/introduction.tex	Sat Jan 30 15:00:31 2021 +0900
+++ b/paper/chapter/introduction.tex	Sat Jan 30 16:22:52 2021 +0900
@@ -1,4 +1,4 @@
-\chapter{継続を中心としたプログラミングスタイル}
+\chapter{OSとアプリケーションの信頼性}
 
 コンピューター上では様々なアプリケーションが常時動作している。
 動作しているアプリケーションは信頼性が保証されていてほしい。
@@ -34,6 +34,20 @@
 
 他の形式手法にモデル検査がある。
 モデル検査は実際に動作するコードですべての可能な実行の組み合わせを実行し検証する方法である。
+例えばJavaのソースコードに対してモデル検査をするJavaPathFinderなどがある。
 モデル検査を利用する場合は、実際に動作するコード上で検証を行うことが出来る。
-実装するコードに対してモデル検査を行いたいが、モデル検査を行うモデル検査器は限られている。
-例えばJavaのソースコードに対してモデル検査をするJavaPathFinderなどがある。
+OSのソースコードそのものをモデル検査すると、実際に検証されたOSが動作可能となる。
+しかしOSの処理は膨大であり、 様々な関数呼び出しや非決定的な処理、 並行処理などが発生する。
+モデル検査を行う場合でも、やみくもにOSのすべての処理を検査するのは難しい。
+
+
+OSのシステムコールは、ユーザーからAPI経由で呼び出され、 いくつかの処理を行う。
+その処理に着目するとOSは様々な状態を遷移して処理を行っていると考えることができる。
+OSを巨大な状態遷移マシンと考えると、 OSの処理の特定の状態の遷移まで範囲を絞ることができる。
+範囲が限られているため、有限時間でモデル検査などで検証することが可能である。
+この為にはOSの処理を状態遷移系で表現し、 証明しやすくする必要がある。
+
+
+OSを状態遷移系で実装する場合、通常のC言語では状態ごとに分離するのは困難である。
+関数呼び出しを利用して状態を切り分けても、 関数呼び出し時に伴うスタックフレームの操作などでパフォーマンスにも問題がある。
+この問題を解決するには、 C言語よりも細かく記述できる言語で実装する必要がある。
\ No newline at end of file