--- a/paper/chapter/01-introduction.tex	Tue Feb 02 17:18:59 2021 +0900
+++ b/paper/chapter/01-introduction.tex	Tue Feb 02 18:47:49 2021 +0900
@@ -37,6 +37,10 @@
 しかしOSの処理は膨大である。
 すべての存在可能な状態を数え上げるモデル検査では状態爆発が問題となる。
 状態を有限に制限したり抽象化を行う必要がある。
+また、モデル検査ができるモデル検査器は特定のプログラム形式でないと動かないものがある。
+例えばSpinはPromela形式でないとモデル検査ができない。
+モデル検査ができる場合も、 モデル検査したコードと実際に動くコードを同一にしたい。
+また、モデル検査をする場合としない場合の切り替えを、より手軽に行いたい。
 
 
 OSのシステムコールは、ユーザーからAPI経由で呼び出され、 いくつかの処理を行う。
@@ -65,7 +69,7 @@
 プログラムの整合性の検証はメタレベルの計算で行いたい。
 ユーザーが実装したノーマルレベルの計算に対応するメタレベルの計算を、自由にメタレベルの計算で証明したい。
 またメタレベルで検証ががすでにされたプログラムがあった場合、都度実行ユーザーの環境で検証が行われるとパフォーマンスに問題が発生する。
-この場合はメタレベルの計算を検証をするもの、しないものと切り替えられる柔軟なAPIが必要となる。
+この場合は検証を実行するメタ計算と、 検証をしないメタ計算を手軽に切り替える必要がある。
 メタレベルの計算をノーマルレベルの計算と同等にプログラミングできると、動作するコードに対して様々なアプローチが掛けられる。
 この為にはノーマルレベル、メタレベル共にプログラミングできる言語と環境が必要となる。