\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}
%\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{GearsAgda上のモデル検査の形式化}

%\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であるGearsOSを開発している．
  CbC とは， C言語から通常の関数呼び出しではなく，アセンブラでいうjmp命令により関数を遷移する継続を導入した C 言語の下位言語である．
  すでにGearsOSはメタ計算によるモデル検査機構を持っている．
  GearsOSのCodeGear/DataGearはGearsAgdaにより形式証明に向いた形に記述することができる．
  モデル検査機構をGearsAgdaにより記述することで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 \ref{agda-dpp-bruteforce}
を定義した．


\lstinputlisting[caption= Gears Agdaでの DPP の場合を網羅するコード, label=agda-dpp-bruteforce]{src/agda-dpp-modelcheck.agda.replaced}

内部で行っていることとして，その 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}