%%
%% 研究報告用スイッチ
%% [techrep]
%%
%% 欧文表記無しのスイッチ(etitle,eabstractは任意)
%% [noauthor]
%%

%\documentclass[submit,techrep]{ipsj}
\documentclass[submit,techrep,noauthor]{ipsj}



\usepackage[dvips]{graphicx}
\usepackage{latexsym}

\def\Underline{\setbox0\hbox\bgroup\let\\\endUnderline}
\def\endUnderline{\vphantom{y}\egroup\smash{\underline{\box0}}\\}
\def\|{\verb|}
%

%\setcounter{巻数}{59}%vol59=2018
%\setcounter{号数}{10}
%\setcounter{page}{1}


\begin{document}


\title{xv6の構成要素の継続の分析}

%\etitle{How to Prepare Your Paper for IPSJ SIG Technical Report \\ (version 2018/10/29)}

\affiliate{KIE}{琉球大学大学院理工学研究科情報工学専攻}
\affiliate{IE}{琉球大学工学部工学科知能情報コース}


\author{清水 隆博}{Shimizu Takahiro}{KIE}[anatofuz@cr.ie.u-ryukyu.ac.jp]
\author{河野 真治}{Shinji Kono}{IE}[kono@ie.u-ryukyu.ac.jp]

\begin{abstract}
OS自体そのものは高い信頼性が求められるが、 OSを構成するすべての処理をテストするのは困難である。
テストを利用して信頼性を高めるのではなく、 OSの状態を状態遷移を基本としたモデルに変換し形式手法を用いて信頼性を高めたい。

状態遷移単位での記述に適した言語であるCbCを用いて、小さなunixであるxv6 kernelの書き換えを行っている。
このためには現状のxv6 kernelの処理がどのような状態遷移を行うのかを分析し、継続ベースでのプログラミングに変換していく必要がある。
本稿ではxv6kernelの構成要素の一部に着目し、状態遷移系の分析と状態遷移系を元に継続ベースでxv6の再実装を行う。
\end{abstract}


\maketitle