--- a/paper/md2tex/first.tex	Thu May 07 16:25:28 2020 +0900
+++ b/paper/md2tex/first.tex	Thu May 07 16:33:47 2020 +0900
@@ -63,12 +63,14 @@
 \author{河野 真治}{Shinji Kono}{IE}[kono@ie.u-ryukyu.ac.jp]
 
 \begin{abstract}
-OS自体そのものは高い信頼性が求められるが、 OSを構成するすべての処理をテストするのは困難である。
-テストを利用して信頼性を高めるのではなく、 OSの状態を状態遷移を基本としたモデルに変換し形式手法を用いて信頼性を高めたい。
-
-状態遷移単位での記述に適した言語であるCbCを用いて、小さなunixであるxv6 kernelの書き換えを行っている。
-このためには現状のxv6 kernelの処理がどのような状態遷移を行うのかを分析し、継続ベースでのプログラミングに変換していく必要がある。
-本稿ではxv6kernelの構成要素の一部に着目し、状態遷移系の分析と状態遷移系を元に継続ベースでxv6の再実装を行う。
+アプリケーションやサービスの信頼性は、OSと結びついている。OS自身が高い信頼性を持つ必要があり、
+その上で動作するソフトウェアの信頼性をOSが保証するような仕組みがあると良い。
+テストは本質的に有限なケースしか調べないので、テストだけで信頼性を保証するのには限界がある。
+アプリケーションとOSの状態を状態遷移を基本としたモデルに変換しモデル検査やHoare Logic などの形式手法を用いて信頼性を高めたい。
+そのために状態遷移単位での記述に適した継続を基本とした言語であるCbC(Continuation based C)をOSとアプリケーションの記述に用いる。
+最初の段階として小さなunixであるxv6 kernelのCbCによる書き換えを行っている。
+xv6 kernelの処理がどのような状態遷移を行うのかを分析し、CbCの継続ベースでのプログラミングに変換していく必要がある。
+本稿ではxv6kernelの構成要素の一部に着目し、状態遷移系の分析とxv6の書き換えを行う。
 \end{abstract}