% withpage: ページ番号をつける (著者確認用)
% english: 英語原稿用フォーマット
\documentclass{ipsjprosym}
%\documentclass[withpage, english]{ipsjprosym}

\usepackage[dvipdfmx]{graphicx}
\usepackage{latexsym}
\usepackage{comment}
\usepackage{listings}
\usepackage{here}
\lstset{
  language=C, 
  tabsize=2, 
  frame=single, 
  basicstyle={\tt\footnotesize}, % 
  identifierstyle={\footnotesize}, % 
  commentstyle={\footnotesize\itshape}, % 
  keywordstyle={\footnotesize\ttfamily}, % 
  ndkeywordstyle={\footnotesize\ttfamily}, % 
  stringstyle={\footnotesize\ttfamily}, 
  breaklines=true, 
  captionpos=b, 
  columns=[l]{fullflexible}, % 
  xrightmargin=0zw, % 
  xleftmargin=1zw, % 
  aboveskip=1zw, 
  numberstyle={\scriptsize}, % 
  stepnumber=1, 
  numbersep=0.5zw, % 
  lineskip=-0.5ex, 
}
\renewcommand{\lstlistingname}{Code}
\usepackage{caption}
\captionsetup[lstlisting]{font={small, tt}}
\usepackage{url}
\begin{document}

% Title,  Author %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\title{継続を基本としたOS Gears OS}

%\affiliate{IPSJ}{情報処理学会}
\affiliate{KRYUKYU}{琉球大学大学院理工学研究科情報工学専攻}
\affiliate{IERYUKYU}{琉球大学工学部情報工学科}

\author{清水 隆博}{Takahiro SHIMIZU}{KRYUKYU}[anatofuz@cr.ie.u-ryukyu.ac.jp]
\author{河野 真治}{Shinji KONO}{IERYUKYU}[kono@ie.u-ryukyu.ac.jp]

%概要
\begin{abstract}
継続を基本とするCと互換性のある言語、 Conitinuation Based C(CbC)を用いてOSの実装を考案した。
状態遷移単位でOSの処理を実装することで、 処理の入出力が明確化され、 定理証明支援系に適した表現形式で処理が記述可能である。
ここでは現在CbCを用いて開発しているOS、 GearsOSについての実装及び今後の展望について考察する。
\end{abstract}

\begin{jkeyword}
システムプログラミング, CbC, 軽量継続, OS
\end{jkeyword}

\maketitle

% Body %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{証明可能なOS}
コンピュータ上で動作するあらゆるソフトウェアや資源を管理するOSは、 高い信頼性が保証されてほしい。
信頼性の保証にはテストプログラムを用いた検証や、 形式手法を用いた証明を使う手法が存在する。
頻繁に並列処理を行うOSでは、 スレッド間の共通資源の競合などの非決定的な実行を行う。
OSの信頼性を保証する上ではテストやデバッグを用いる手法では、 発生しうる状態を完全に保証するのは困難である。
テストを用いる方法ではなく、 形式手法的なアプローチを用いてOSの信頼性を保証したい。
そのためには定理証明支援系などで証明が可能な形式と、 等価な形式でOSを記述する必要性がある。
現在開発しているGearsOSは、 継続を基本とする言語Conitinuation Based C(CbC)で実装されている。
CbCは状態遷移単位での実行であり、 他の状態に遷移する際に今までの環境を持たない。
そのため、 CbCで実装した処理は入出力が明確化され、 定理証明支援系で表現可能な形式にする事が可能である。


\nocite{*}
\bibliographystyle{ipsjsort}
\bibliography{reference}

\end{document}