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

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



\usepackage[dvips,dvipdfmx]{graphicx}
\usepackage{latexsym}
\usepackage{listings}
\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,
}
\usepackage{caption}


\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}
\renewcommand{\lstlistingname}{Code}

\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が保証するような仕組みがあると良い。
テストは本質的に有限なケースしか調べないので、テストだけで信頼性を保証するのには限界がある。
アプリケーションとOSの状態を状態遷移を基本としたモデルに変換しモデル検査やHoare Logic などの形式手法を用いて信頼性を高めたい。
そのために状態遷移単位での記述に適した継続を基本とした言語であるCbC(Continuation based C)をOSとアプリケーションの記述に用いる。
最初の段階として小さなunixであるxv6 kernelのCbCによる書き換えを行っている。
xv6 kernelの処理がどのような状態遷移を行うのかを分析し、CbCの継続ベースでのプログラミングに変換していく必要がある。
本稿ではxv6kernelの構成要素の一部に着目し、状態遷移系の分析とxv6の書き換えを行う。
\end{abstract}


\maketitle