# HG changeset patch
# User anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
# Date 1574231003 -32400
# Node ID bee0603ddad4ce4981fe4519760a53e650ed71f1
# Parent  b6c782f35e4ff60609b948573e002973c5711129
tweak

diff -r b6c782f35e4f -r bee0603ddad4 paper/anatofuz_prosym_2019.pdf
Binary file paper/anatofuz_prosym_2019.pdf has changed
diff -r b6c782f35e4f -r bee0603ddad4 paper/anatofuz_prosym_2019.tex
--- a/paper/anatofuz_prosym_2019.tex	Wed Nov 20 15:19:04 2019 +0900
+++ b/paper/anatofuz_prosym_2019.tex	Wed Nov 20 15:23:23 2019 +0900
@@ -47,9 +47,9 @@
 
 %概要
 \begin{abstract}
-継続を基本とするCと互換性のある言語、Conitinuation Based C(CbC)を用いてOSの実装を考案した。
-状態遷移単位でOSの処理を実装することで、入出力が明確化され、定理証明支援系などとの表現形式と同様の表現で動作が記述可能である。
-ここでは現在CbCを用いて開発しているGearsOSについての実装及び今後の展望について考察する。
+継続を基本とするCと互換性のある言語、 Conitinuation Based C(CbC)を用いてOSの実装を考案した。
+状態遷移単位でOSの処理を実装することで、 処理の入出力が明確化され、 定理証明支援系に適した表現形式で処理が記述可能である。
+ここでは現在CbCを用いて開発しているOS、 GearsOSについての実装及び今後の展望について考察する。
 \end{abstract}
 
 \begin{jkeyword}
@@ -62,6 +62,8 @@
 \section{証明可能なOS}
 コンピュータ上で動作するあらゆるソフトウェアや資源を管理するOSは、 高い信頼性が保証されるべきである。
 信頼性の保証にはテストプログラムを用いた検証や、 形式手法を用いた証明を使う手法が存在する。
+頻繁に並行処理を行うOSでは、 テストを用いてバグを発見するのが困難である。
+そのため、 形式手法的なアプローチを用いてOSの信頼性を保証したい。
 現在開発しているGearsOSは、 継続を基本とする言語Conitinuation Based C(CbC)で実装されている。