Mercurial > hg > Papers > 2019 > anatofuz-prosym-gears

comparison paper/anatofuz_prosym_2019.tex @ 2:bee0603ddad4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tweak
author anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
date Wed, 20 Nov 2019 15:23:23 +0900
parents b6c782f35e4f
children 450d0e91835b
comparison
equal deleted inserted replaced
1:b6c782f35e4f 2:bee0603ddad4
45 \author{清水 隆博}{Takahiro SHIMIZU}{KRYUKYU}[anatofuz@cr.ie.u-ryukyu.ac.jp] 45 \author{清水 隆博}{Takahiro SHIMIZU}{KRYUKYU}[anatofuz@cr.ie.u-ryukyu.ac.jp]
46 \author{河野 真治}{Shinji KONO}{IERYUKYU}[kono@ie.u-ryukyu.ac.jp] 46 \author{河野 真治}{Shinji KONO}{IERYUKYU}[kono@ie.u-ryukyu.ac.jp]
47 47
48 %概要 48 %概要
49 \begin{abstract} 49 \begin{abstract}
50 継続を基本とするCと互換性のある言語、Conitinuation Based C(CbC)を用いてOSの実装を考案した。 50 継続を基本とするCと互換性のある言語、 Conitinuation Based C(CbC)を用いてOSの実装を考案した。
51 状態遷移単位でOSの処理を実装することで、入出力が明確化され、定理証明支援系などとの表現形式と同様の表現で動作が記述可能である。 51 状態遷移単位でOSの処理を実装することで、 処理の入出力が明確化され、 定理証明支援系に適した表現形式で処理が記述可能である。
52 ここでは現在CbCを用いて開発しているGearsOSについての実装及び今後の展望について考察する。 52 ここでは現在CbCを用いて開発しているOS、 GearsOSについての実装及び今後の展望について考察する。
53 \end{abstract} 53 \end{abstract}
54 54
55 \begin{jkeyword} 55 \begin{jkeyword}
56 システムプログラミング, CbC, 軽量継続, OS 56 システムプログラミング, CbC, 軽量継続, OS
57 \end{jkeyword} 57 \end{jkeyword}
60 60
61 % Body %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 61 % Body %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
62 \section{証明可能なOS} 62 \section{証明可能なOS}
63 コンピュータ上で動作するあらゆるソフトウェアや資源を管理するOSは、 高い信頼性が保証されるべきである。 63 コンピュータ上で動作するあらゆるソフトウェアや資源を管理するOSは、 高い信頼性が保証されるべきである。
64 信頼性の保証にはテストプログラムを用いた検証や、 形式手法を用いた証明を使う手法が存在する。 64 信頼性の保証にはテストプログラムを用いた検証や、 形式手法を用いた証明を使う手法が存在する。
65 頻繁に並行処理を行うOSでは、 テストを用いてバグを発見するのが困難である。
66 そのため、 形式手法的なアプローチを用いてOSの信頼性を保証したい。
65 現在開発しているGearsOSは、 継続を基本とする言語Conitinuation Based C(CbC)で実装されている。 67 現在開発しているGearsOSは、 継続を基本とする言語Conitinuation Based C(CbC)で実装されている。
66 68
67 69
68 70
69 \nocite{*} 71 \nocite{*}