# HG changeset patch
# User ikkun <ikkun@cr.ie.u-ryukyu.ac.jp>
# Date 1588316195 -32400
# Node ID 88ac3c6db36772be5bf4c02a3d50622d6ada48fb
# Parent  f108fda488f97eaa3d969742f20329f0a1a7d1b4
add maindmap

diff -r f108fda488f9 -r 88ac3c6db367 mindmap.mm
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/mindmap.mm	Fri May 01 15:56:35 2020 +0900
@@ -0,0 +1,1 @@
+<map version="0.9.0"><node TEXT="GearsOSでモデル検査を実現する手法について" ID="aiakscgq"><node TEXT="モデル検査" ID="ufwvowvu" POSITION="right"><node TEXT="並列プログラム" ID="obwguirr"/><node TEXT="Java path findar" ID="vvocnvqs"><node TEXT="javaのバイトコード" ID="diroqvur"/><node TEXT="複数プロセス不可" ID="eylzlwcg"/><node TEXT="大規模コード不可" ID="ukcpntxd"/><node TEXT="検出可能なもの" ID="zjwyspdv"><node TEXT="アサーション" ID="neugnpag"/><node TEXT="デッドロック" ID="wragddos"/><node TEXT="キャッチされていない例外" ID="twciuneh"/></node></node><node TEXT="SPIN" ID="hxwpbcxv"><node TEXT="PROMELA" ID="jbbtfpzb"><node TEXT="プログラム変換が必要" ID="kiqcqrqn"/><node TEXT="Cの検証器を生成する" ID="adjzlwnf"><node TEXT="コンパイル、実行で検証" ID="xmmmhkcc"/></node><node TEXT="検出可能なもの" ID="ydirxprc"><node TEXT="アサーション" ID="bmjrldll"/><node TEXT="デッドロック" ID="iihcqipk"/><node TEXT="到達生" ID="olydrtho"/><node TEXT="進行性" ID="fglnjswe"/><node TEXT="LTL式" ID="fyfjnzfi"/></node></node></node><node TEXT="タブロー展開" ID="gwizogpi"><node TEXT="実行可能な組み合わせを全て調べる" ID="nrukdnoc"/><node TEXT="深さ優先探索" ID="ahiasxly"/><node TEXT="状態はTreeで記録" ID="kltjozbv"/><node TEXT="同じ状態は共有される" ID="sruoxtze"/></node></node><node TEXT="GearsOS" ID="kxsdxumx" POSITION="right"><node TEXT="CbC" ID="kpiqygux"><node TEXT="軽量継続" ID="xqplqjoh"/><node TEXT="par goto" ID="nccdilvu"/><node TEXT="code gear data gear" ID="ukgxltmd"/><node TEXT="meta gear" ID="cnfvrtmr"/></node></node><node TEXT="DPP" ID="ycbpofai" POSITION="right"><node TEXT="dining philosopher problem とは" ID="ghljpzez"/><node TEXT="資源共有問題" ID="zsdzbetp"><node TEXT="デッドロック" ID="uugrmdug"/></node><node TEXT="CbCによる実装" ID="tcqjjdut"><node TEXT="philosopher のthread実装" ID="qkyujslq"/><node TEXT="並列化" ID="vxgdwprc"><node TEXT="par gotoとforkでの並列化" ID="twhbnikf"><node TEXT="synchro nized queue　による排他的制御" ID="glokmulp"/></node></node><node TEXT="scheduler" ID="xhnmftto"><node TEXT="queue" ID="huneevce"><node TEXT="iteretor" ID="yuaezsaw"/></node></node></node></node><node TEXT="課題" ID="crljrupm" POSITION="right"><node TEXT="モデル検査における状態数の多さ" ID="radpfpcl"/><node TEXT="GearsOSにおける制御は割り込みがないため、I/Oの途中で書き込みが負ける可能性" ID="gfbqapsf"/><node TEXT="排他的制御とシングルスレッドの検証の相性を考えないといけない" ID="rngykwag"/></node></node></map>
\ No newline at end of file
diff -r f108fda488f9 -r 88ac3c6db367 paper/ikkun-sigos.pdf
Binary file paper/ikkun-sigos.pdf has changed
diff -r f108fda488f9 -r 88ac3c6db367 paper/ikkun-sigos.tex
--- a/paper/ikkun-sigos.tex	Tue Apr 28 16:34:29 2020 +0900
+++ b/paper/ikkun-sigos.tex	Fri May 01 15:56:35 2020 +0900
@@ -27,29 +27,19 @@
 \begin{document}
 
 
-\title{情報処理学会研究報告の準備方法\\
-（2018年10月29日版）}
+\title{Gears OSでモデル検査を実現する手法について}
 
-\etitle{How to Prepare Your Paper for IPSJ SIG Technical Report \\ (version 2018/10/29)}
-
-\affiliate{IPSJ}{情報処理学会\\
-IPSJ, Chiyoda, Tokyo 101--0062, Japan}
+\affiliate{1}{琉球大学大学院理工学研究科情報工学専攻}
+\affiliate{2}{琉球大学工学部工学科知能情報コース}
+\affiliate{3}{琉球大学工学部}
 
 
-\paffiliate{JU}{情報処理大学\\
-Johoshori Uniersity}
-
-\author{情報 太郎}{Joho Taro}{IPSJ}[joho.taro@ipsj.or.jp]
-\author{処理 花子}{Shori Hanako}{IPSJ}
-\author{学会 次郎}{Gakkai Jiro}{IPSJ,JU}[gakkai.jiro@ipsj.or.jp]
+\author{東恩納　琢偉}{Takui Higashionna}{1}[ikkun@cr.ie.u-ryukyu.ac.jp
+\author{奥田　光希}{Okuda Kouki}{2}[Koki.okuda@cr.ie.u-ryukyu.ac.jp]
+\author{河野　真治}{Shinji kono}{3}[kono@ie.u-ryukyu.ac.jp]
 
-\begin{abstract}
-本稿は，情報処理学会研究報告に投稿する原稿を執筆する際の注意点等をまとめたものである．
-\LaTeX と専用のスタイルファイルを用いた場合の論文フォーマットに関する指針，
-および論文の内容に関してするべきこと，
-するべきでないことをまとめたべからずチェックリストからなる．
-本稿自体も\LaTeX と専用のスタイルファイルを用いて執筆されているため，
-論文執筆の際に参考になれば幸いである．
+\begin{abstract}}
+GeasOSはCbCで記述されており処理単位であるcodeGearの間に自由にメタ計算をはさむことができる。ここにdataGearの状態を記録することにより、ユーザプロセスあるいはカーネルそのもののモデル検査が可能になる。一般的なモデル検査では状態数の爆発は避けられない。記録する状態を抽象化あるいは限定する手法について考察する。
 \end{abstract}
 
 
@@ -73,16 +63,7 @@
 \maketitle
 
 %1
-\section{はじめに}
-
-情報処理学会では，研究報告の発行を行っている．
-
-本稿では，まずそのスタイルファイルを用いた論文のフォーマットに関して述べる．
-新たなスタイルファイルでは，
-極力特別なコマンドは使わずに，標準的な\LaTeX のスタイルを踏襲している．
-論文フォーマットに関しては，\ref{sec:format}~章で後述する指針に従って頂くが，
-そこに規定されていること以外は標準的な\LaTeX のコマンドをそのまま使うことができる．
-本稿は，そのスタイルファイルを実際に使っているので，論文執筆の際に参考にされたい．
+\section{モデル検査}