<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>