changeset 2:bee0603ddad4

tweak
author anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
date Wed, 20 Nov 2019 15:23:23 +0900
parents b6c782f35e4f
children 450d0e91835b
files paper/anatofuz_prosym_2019.pdf paper/anatofuz_prosym_2019.tex
diffstat 2 files changed, 5 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
Binary file paper/anatofuz_prosym_2019.pdf has changed
--- 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)で実装されている。