\AtBeginDvi{\special{pdf:mapfile ptex-ipa.map}}
\documentclass[submit,techrep,noauthor]{ipsj}
%\usepackage{graphicx}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{textcomp}
\usepackage{latexsym}
%\usepackage[fleqn]{amsmath}
%\usepackage{amssymb}
\usepackage{listings}
\usepackage[dvipdfmx]{graphicx}
\usepackage{graphicx}
\usepackage{lmodern}
\usepackage{textcomp}
\usepackage{latexsym}
\usepackage{ascmac}
\usepackage[fleqn]{amsmath}
\usepackage{amssymb}
\usepackage[deluxe, multi]{otf}
\usepackage{url}
\usepackage{cite}
\usepackage{svg}
%\documentclass[withpage, english]{ipsjprosym}
%\usepackage{comment}
\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, 
  escapechar=\!,
}
\usepackage{caption}
\newcommand\newblock{\hskip .11em\@plus.33em\@minus.07em}
\captionsetup[lstlisting]{font={small, tt}}

\renewcommand{\lstlistingname}{Code}


\begin{document}

% Title,  Author %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\title{Gears Agda 上のモデル検査の形式化}

%\affiliate{IPSJ}{情報処理学会}
\affiliate{IIRYUKYU}{琉球大学大学院理工学研究科工学専攻知能情報プログラム}
\affiliate{IERYUKYU}{琉球大学大学工学部工学科知能情報コース}

\author{上地 悠斗}{Yuto UECHI}{IIRYUKYU}[soto@cr.ie.u-ryukyu.ac.jp]
\author{河野 真治}{Shinji KONO}{IERYUKYU}[kono@ie.u-ryukyu.ac.jp]

%概要
\begin{abstract}
  当研究室では Continuation based C （CbC） という言語を用いて，拡張性と信頼性を両立する OS である Gears OS を開発している．
  CbC とは， C言語から通常の関数呼び出しではなく，アセンブラでいうjmp命令により関数を遷移する継続を導入した C 言語の下位言語である．
  すでに Gears OS はメタ計算によるモデル検査機構を持っている．
   GearsOS の CodeGear/DataGear は Gears Agda により形式証明に向いた形に記述することができる．
  モデル検査機構を Gears Agda により記述することで Hoare Logic 的な逐次実行型のプログラムの証明だけでなく，並行実行を含むプログラムの証明が可能になる．
\end{abstract}

\maketitle

% Body %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\input{tex/intro.tex} % はじめに　
\input{tex/cbc.tex} % cbc の説明 軽く
% \input{tex/agda.tex} % agda の説明　もしかしたらいるかも
\input{tex/cbc_agda.tex}% Gears Agda の記法　loopのやつやる

\section{モデル検査}
モデル検査とは，検証手法の一つである．
他の検証手法として代表的なものとして，定理証明が挙げられる．

モデル検査はプログラムが入力に対して仕様を満たした動作を
行うことを網羅的に検証することを指す．

モデル検査と定理証明を比較した際に，モデル検査は入力が無限になる
状態爆発が起こり得るという問題がある．
定理証明では数学的な証明をするため状態爆発を起こさず検証を行うことが
できるが，専門的な知識が多く難易度が高いという欠点がある．

\input{tex/dpp_impl.tex}% Gears Agda の記法　loopのやつやる

\section{DPP のモデル検査}
モデル検査の機能として，入力の網羅が挙げられる．
今回の DPP の入力の網羅として，哲学者が思考をつづけるのか，食事をはじめようとするのかと
食事中に食事をそのままつづけるのか，思考をするために食事を止めようとするのかが分岐する．

そのため， next-code が thinking か eating であるものに対して分岐を網羅するコードを実装した．

内部で行っていることとして，その Code Gear 内に存在している next-code が thinking もしくは eating である場合に
そのプロセスの next-code をそのままにするか，それぞれ pickup-rfork か putdown-lfork にする．
そのため，その部分に対して bit 全探索を行い，場合の網羅を行っている．

% まとめ

\section{まとめと今後の課題}
今回は Agda に CbC の継続の概念を追加した Gears Agda にて DPP のモデル検査を行おうとした．
結果として，DPP の実装と入力の網羅までできた．

今後はプロセスがすべてほかのプロセスの終了待ちになった場合に dead lock 状態になっていることを検知できるようにしたい．
加えて，assert の機能をつけて仕様通りの動作がされていることを検証したい．
 
\nocite{*}
\bibliographystyle{ipsjsort}
\bibliography{reference}

\end{document}