Mercurial > hg > Papers > 2020 > ikkun-sigos

changeset 29:d460c442d596

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author ikkun <ikkun@cr.ie.u-ryukyu.ac.jp>
date Thu, 28 May 2020 09:06:39 +0900
parents 43d413be71c4
children 1048f5e71d91
files presen/sigos.html presen/sigos.md
diffstat 2 files changed, 72 insertions(+), 69 deletions(-) [+]
line wrap: on
line diff
--- a/presen/sigos.html	Thu May 28 01:39:29 2020 +0900
+++ b/presen/sigos.html	Thu May 28 09:06:39 2020 +0900
@@ -12,7 +12,7 @@
 
 /* @theme example */div#p>svg>foreignObject>section{background-image:url("assets/logo.svg");background-position:right 3% bottom 2%;background-repeat:no-repeat;background-attachment:5%;background-size:20% auto}
 
-/* @theme za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj */div#p>svg>foreignObject>section[data-marpit-advanced-background=background]{display:block!important;padding:0!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]:after,div#p>svg>foreignObject>section[data-marpit-advanced-background=background]:before,div#p>svg>foreignObject>section[data-marpit-advanced-background=content]:after,div#p>svg>foreignObject>section[data-marpit-advanced-background=content]:before{display:none!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container]{all:initial;display:flex;flex-direction:row;height:100%;overflow:hidden;width:100%}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container][data-marpit-advanced-background-direction=vertical]{flex-direction:column}div#p>svg>foreignObject>section[data-marpit-advanced-background=background][data-marpit-advanced-background-split]>div[data-marpit-advanced-background-container]{width:var(--marpit-advanced-background-split,50%)}div#p>svg>foreignObject>section[data-marpit-advanced-background=background][data-marpit-advanced-background-split=right]>div[data-marpit-advanced-background-container]{margin-left:calc(100% - var(--marpit-advanced-background-split, 50%))}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container]>figure{all:initial;background-position:center;background-repeat:no-repeat;background-size:cover;flex:auto;margin:0}div#p>svg>foreignObject>section[data-marpit-advanced-background=content],div#p>svg>foreignObject>section[data-marpit-advanced-background=pseudo]{background:transparent!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=pseudo],div#p>svg[data-marpit-svg]>foreignObject[data-marpit-advanced-background=pseudo]{pointer-events:none!important}div#p>svg>foreignObject>section[data-marpit-advanced-background-split]{width:100%;height:100%}</style></head><body><div class="bespoke-marp-osc"><button data-bespoke-marp-osc="prev" tabindex="-1" title="Previous slide">Previous slide</button><span data-bespoke-marp-osc="page"></span><button data-bespoke-marp-osc="next" tabindex="-1" title="Next slide">Next slide</button><button data-bespoke-marp-osc="fullscreen" tabindex="-1" title="Toggle fullscreen (f)">Toggle fullscreen</button><button data-bespoke-marp-osc="presenter" tabindex="-1" title="Open presenter view (p)">Open presenter view</button></div><div id="p"><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="1" data-paginate="true" data-theme="za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj" data-marpit-pagination="1" data-marpit-pagination-total="20" style="--paginate:true;--theme:za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj;">
+/* @theme cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme */div#p>svg>foreignObject>section[data-marpit-advanced-background=background]{display:block!important;padding:0!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]:after,div#p>svg>foreignObject>section[data-marpit-advanced-background=background]:before,div#p>svg>foreignObject>section[data-marpit-advanced-background=content]:after,div#p>svg>foreignObject>section[data-marpit-advanced-background=content]:before{display:none!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container]{all:initial;display:flex;flex-direction:row;height:100%;overflow:hidden;width:100%}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container][data-marpit-advanced-background-direction=vertical]{flex-direction:column}div#p>svg>foreignObject>section[data-marpit-advanced-background=background][data-marpit-advanced-background-split]>div[data-marpit-advanced-background-container]{width:var(--marpit-advanced-background-split,50%)}div#p>svg>foreignObject>section[data-marpit-advanced-background=background][data-marpit-advanced-background-split=right]>div[data-marpit-advanced-background-container]{margin-left:calc(100% - var(--marpit-advanced-background-split, 50%))}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container]>figure{all:initial;background-position:center;background-repeat:no-repeat;background-size:cover;flex:auto;margin:0}div#p>svg>foreignObject>section[data-marpit-advanced-background=content],div#p>svg>foreignObject>section[data-marpit-advanced-background=pseudo]{background:transparent!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=pseudo],div#p>svg[data-marpit-svg]>foreignObject[data-marpit-advanced-background=pseudo]{pointer-events:none!important}div#p>svg>foreignObject>section[data-marpit-advanced-background-split]{width:100%;height:100%}</style></head><body><div class="bespoke-marp-osc"><button data-bespoke-marp-osc="prev" tabindex="-1" title="Previous slide">Previous slide</button><span data-bespoke-marp-osc="page"></span><button data-bespoke-marp-osc="next" tabindex="-1" title="Next slide">Next slide</button><button data-bespoke-marp-osc="fullscreen" tabindex="-1" title="Toggle fullscreen (f)">Toggle fullscreen</button><button data-bespoke-marp-osc="presenter" tabindex="-1" title="Open presenter view (p)">Open presenter view</button></div><div id="p"><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="1" data-paginate="true" data-theme="cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme" data-marpit-pagination="1" data-marpit-pagination-total="20" style="--paginate:true;--theme:cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme;">
 <h1><svg data-marp-fitting="svg"><foreignObject><span data-marp-fitting-svg-content> Gears OSでモデル検査を実現する手法について</span></foreignObject></svg></h1>
 <ul>
 <li>東恩納 琢偉
@@ -22,15 +22,15 @@
 </li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="2" data-paginate="true" data-theme="za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj" data-marpit-pagination="2" data-marpit-pagination-total="20" style="--paginate:true;--theme:za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="2" data-paginate="true" data-theme="cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme" data-marpit-pagination="2" data-marpit-pagination-total="20" style="--paginate:true;--theme:cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme;">
 <h1>研究目的</h1>
 <ul>
 <li>OS上ではさまざまなアプリケーションやサービスが提供されるが、予期しないエラーが起こり得る。</li>
 <li>本研究室で開発している GearsOS ではアプリケーションやサービスの信頼性をOSの機能として保証することを目指しており、今回はモデル検査による信頼性の保証について考察する。</li>
-<li>またGearsOS そのものをGearsOS上でモデル検査することに関しても考察する。</li>
+<li>またGearsOS そのものをGearsOS上でモデル検査する手法について考察する。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="3" data-paginate="true" data-theme="za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj" data-marpit-pagination="3" data-marpit-pagination-total="20" style="--paginate:true;--theme:za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="3" data-paginate="true" data-theme="cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme" data-marpit-pagination="3" data-marpit-pagination-total="20" style="--paginate:true;--theme:cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme;">
 <h1>Gears OS</h1>
 <ul>
 <li>軽量継続を基本とする言語 Contnution based C を用いて記述されている。</li>
@@ -38,10 +38,10 @@
 <li>信頼性を保証する方法としてモデル検査による検証や、定理証明を用いる事で、信頼性へのアプローチを行っています。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="4" data-paginate="true" data-theme="za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj" data-marpit-pagination="4" data-marpit-pagination-total="20" style="--paginate:true;--theme:za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="4" data-paginate="true" data-theme="cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme" data-marpit-pagination="4" data-marpit-pagination-total="20" style="--paginate:true;--theme:cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme;">
 <h1>Continution based C</h1>
 <ul>
-<li>CbC とは C言語をベースとして、開発された言語でC言語との違いはプログラムにおける goto 文を用いて CodeGear　という単位で遷移する。</li>
+<li>CbC とは C言語をベースとして、開発された言語でC言語との違いはプログラムにおける goto 文を用いて CodeGear という単位で遷移する。</li>
 <li>goto 文による遷移は関数呼び出しとは異なり、stackや環境を隠して持つことがない。</li>
 <li>以下は CbC によって記述された codeGear です。</li>
 </ul>
@@ -57,7 +57,7 @@
 }
 </span></span></foreignObject></svg></code></pre>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="5" data-paginate="true" data-theme="za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj" data-marpit-pagination="5" data-marpit-pagination-total="20" style="--paginate:true;--theme:za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="5" data-paginate="true" data-theme="cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme" data-marpit-pagination="5" data-marpit-pagination-total="20" style="--paginate:true;--theme:cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme;">
 <h1>goto</h1>
 <ul>
 <li>goto 文はCbC における状態遷移に使われ、 goto の直後に遷移先を記述することで接続される。</li>
@@ -66,7 +66,7 @@
 </ul>
 <center><img src="./pic/input-outputDataSegment.svg" alt="" width="100%" height="100%" /></center>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="6" data-paginate="true" data-theme="za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj" data-marpit-pagination="6" data-marpit-pagination-total="20" style="--paginate:true;--theme:za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="6" data-paginate="true" data-theme="cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme" data-marpit-pagination="6" data-marpit-pagination-total="20" style="--paginate:true;--theme:cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme;">
 <h1>dataGear と meta dataGear</h1>
 <ul>
 <li>CbC における入力は dataGear と呼ばれる構造体になっており、ノーマルレベル<br />
@@ -74,7 +74,7 @@
 <li>メタレベルには計算を行うCPUやメモリ、計算に関するノーマルレベルのdataGearを格納するcontext などがある。context は一般的なOSのプロセスに相当する。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="7" data-paginate="true" data-theme="za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj" data-marpit-pagination="7" data-marpit-pagination-total="20" style="--paginate:true;--theme:za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="7" data-paginate="true" data-theme="cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme" data-marpit-pagination="7" data-marpit-pagination-total="20" style="--paginate:true;--theme:cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme;">
 <h1>stub CodeGear</h1>
 <ul>
 <li>メタレベルから見ると、code Gearの入力はcontext ただ1つである。</li>
@@ -93,15 +93,15 @@
 } 
 </span></span></foreignObject></svg></code></pre>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="8" data-paginate="true" data-theme="za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj" data-marpit-pagination="8" data-marpit-pagination-total="20" style="--paginate:true;--theme:za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj;">
-<h1>cotntextと状態数</h1>
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="8" data-paginate="true" data-theme="cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme" data-marpit-pagination="8" data-marpit-pagination-total="20" style="--paginate:true;--theme:cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme;">
+<h1>contextと状態数</h1>
 <ul>
 <li>プログラムの非決定的な実行は、入力あるいは並列実行の非決定性から生じる。</li>
 <li>並列実行の非決定性は、同時に実行される codeGear の順列並び替えになるので、それらの並び替えを生成し、その際に生じるcontextの状態を数え上げる事で、モデル検査を実装できる。</li>
 <li>しかし、このcontextの状態はとても巨大になる事がある、そのためそれらを抽象化する必要性がある。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="9" data-paginate="true" data-theme="za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj" data-marpit-pagination="9" data-marpit-pagination-total="20" style="--paginate:true;--theme:za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="9" data-paginate="true" data-theme="cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme" data-marpit-pagination="9" data-marpit-pagination-total="20" style="--paginate:true;--theme:cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme;">
 <h1>GearsOSの実装</h1>
 <ul>
 <li>codeGear は処理の基本単位であり、並列処理などにより割り込まれることなく記述された通りに実行される必要がある。</li>
@@ -109,21 +109,21 @@
 <li>しかし、GearsOSにおいては正しく実行される事を保証されるように実装されているとする。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="10" data-paginate="true" data-theme="za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj" data-marpit-pagination="10" data-marpit-pagination-total="20" style="--paginate:true;--theme:za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="10" data-paginate="true" data-theme="cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme" data-marpit-pagination="10" data-marpit-pagination-total="20" style="--paginate:true;--theme:cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme;">
 <h1>モデル検査</h1>
 <ul>
 <li>モデルとは検証したいアプリケーションやサービスの振る舞いや性質を抽象化して表現したものであり、抽象化の手法には以下のようなものがある。</li>
-<li>このモデルが仕様を満たしているかどうかを検査するものである。</li>
 </ul>
 <p>状態遷移モデル<br />
 論理モデル<br />
 組み合わせモデル<br />
 フローモデル ..etc</p>
 <ul>
+<li>このモデルが仕様を満たしているかどうかを検査するのがモデル検査である。</li>
 <li>検査の要点によってモデルを使い分ける必要性がある。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="11" data-paginate="true" data-theme="za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj" data-marpit-pagination="11" data-marpit-pagination-total="20" style="--paginate:true;--theme:za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="11" data-paginate="true" data-theme="cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme" data-marpit-pagination="11" data-marpit-pagination-total="20" style="--paginate:true;--theme:cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme;">
 <h1>状態遷移モデル</h1>
 <ul>
 <li>今回行うモデル検査は状態遷移からプログラムの振る舞いを検証する。</li>
@@ -160,15 +160,16 @@
 </tbody>
 </table>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="12" data-paginate="true" data-theme="za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj" data-marpit-pagination="12" data-marpit-pagination-total="20" style="--paginate:true;--theme:za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="12" data-paginate="true" data-theme="cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme" data-marpit-pagination="12" data-marpit-pagination-total="20" style="--paginate:true;--theme:cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme;">
 <h1>既存のモデル検査手法(SPIN)</h1>
 <ul>
+<li>一般的に扱われるモデル検査ツールとしてSPINがある。</li>
 <li>SPIN はPromela (Process Meta Language)で記述される。</li>
 <li>C言語と似た文法を持ち、元は通信プロトコルの検証として開発された言語であり、検証機を生成し、コンパイルと実行を行うことで検証される。</li>
-<li>チャネルを使って通信や並列動作を記述する</li>
+<li>チャネルを使って通信や並列動作を記述する。</li>
 <li>有限オートマトンに変換してモデル検査を行う。</li>
 <li>Promelaへの書き換えが必要</li>
-<li>SPIN では以下の性質を検査可能な性質<br />
+<li>SPIN での検査可能な性質<br />
 アサーション<br />
 デッドロック<br />
 到達性<br />
@@ -176,50 +177,50 @@
 線形時相論理で記述された仕様</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="13" data-paginate="true" data-theme="za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj" data-marpit-pagination="13" data-marpit-pagination-total="20" style="--paginate:true;--theme:za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="13" data-paginate="true" data-theme="cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme" data-marpit-pagination="13" data-marpit-pagination-total="20" style="--paginate:true;--theme:cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme;">
 <h1>既存のモデル検査手法(Java path Finder)</h1>
 <ul>
 <li>Java Path Finder はjavaプログラムの検査ツール</li>
 <li>java バーチャルマシン(JVM) を直接シュミレーション実行している、これによりjavaのバイトコードを直接実行可能である。</li>
 <li>バイトコードを状態遷移モデルとして扱い、実行時に遷移し得る状態を網羅的に検査している。</li>
-<li>実行パターンを網羅的に調べるため、複数のプロセスの取り扱いができず、また状態空間が巨大な場合は、一部を抜き出して実行する必要がある。</li>
-<li>JPF では以下の性質を検査することができる<br />
+<li>実行パターンを網羅的に調べるため、複数のプロセスの取り扱いができず、また状態空間が巨大な場合は、一部を抜き出して検査する必要がある。</li>
+<li>JPF で検査可能な性質<br />
 スレッドの可能な実行すべてを調べる<br />
 デッドロックの検出<br />
 アサーション<br />
 Partial Order Reduction</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="14" data-paginate="true" data-theme="za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj" data-marpit-pagination="14" data-marpit-pagination-total="20" style="--paginate:true;--theme:za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="14" data-paginate="true" data-theme="cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme" data-marpit-pagination="14" data-marpit-pagination-total="20" style="--paginate:true;--theme:cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme;">
 <h1>モデル検査手法について</h1>
 <ul>
 <li>GearsOS におけるモデル検査はcode gear 単位の順列組み合わせによって行われる。</li>
-<li>codegear 実行後の状態を検査し、データベースに格納する。</li>
-<li>新しい上体が生成されなくなった時モデル検査が終了する。</li>
+<li>codegear 実行後の状態を、データベースに格納する。</li>
+<li>新しい状態が生成されなくなった時モデル検査が終了する。</li>
 <li>哲学者５人が次の状態に進めなくなった時をデッドロックとして検出する。</li>
 <li>必要な状態はフォークの状態だけになるので、それ以外の状態は無視することができる。</li>
 <li>これにより状態数を下げることができる。</li>
 <li>つまり、問題に合わせたメタ計算により、モデル検査の状態数を下げることができる。</li>
-<li>GearsOS による検証用プログラムとして Dining Philosohers Ploblem (以下DPP）を用いる。</li>
+<li>GearsOS による検証用プログラムとして Dining Philosohers Ploblem (DPP）を用いる。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="15" data-paginate="true" data-theme="za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj" data-marpit-pagination="15" data-marpit-pagination-total="20" style="--paginate:true;--theme:za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj;">
-<h1>DPP</h1>
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="15" data-paginate="true" data-theme="cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme" data-marpit-pagination="15" data-marpit-pagination-total="20" style="--paginate:true;--theme:cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme;">
+<h1>DPP(dining philosohers ploblem)</h1>
 <ul>
 <li>5人の哲学者が円卓についており、各々スパゲティーの皿が目の前に用意され、スパゲティーは絡まっている為２つのフォーク使わなければ食べれない。</li>
-<li>フォークは席の間に１本ずつある。哲学者は、思考とフォークを持つ、食事する。</li>
+<li>フォークは皿の間に１本ずつの計5本しかないため、すべての哲学者が同時に食事することはできず、また全員がフォークを1本ずつ持ってしまった場合、誰も食事することは出来ない。この状態をデッドロックとする。</li>
 </ul>
-<center><img src="./pic/dpp_image.svg" alt="" width="50%" height="50%" /></center>
+<center><img src="./pic/dpp_image.svg" alt="" width="48%" height="48%" /></center>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="16" data-paginate="true" data-theme="za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj" data-marpit-pagination="16" data-marpit-pagination-total="20" style="--paginate:true;--theme:za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="16" data-paginate="true" data-theme="cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme" data-marpit-pagination="16" data-marpit-pagination-total="20" style="--paginate:true;--theme:cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme;">
 <h1>DPP</h1>
 <ul>
 <li>状態は以下の構成要素からなる<br />
 <code>Pickup Right fork</code> <code> Pickup Left fork</code> <code>eating</code> <code> Put Right fork</code> <code>Put Left fork</code> <code>Thinking</code></li>
 </ul>
-<p><bottom><img src="./pic/dpp_image.svg" alt="" width="70%" height="70%" /></bottom></p>
+<p><bottom><img src="./pic/dpp_image.svg" alt="" width="55%" height="55%" /></bottom></p>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="17" data-paginate="true" data-theme="za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj" data-marpit-pagination="17" data-marpit-pagination-total="20" style="--paginate:true;--theme:za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="17" data-paginate="true" data-theme="cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme" data-marpit-pagination="17" data-marpit-pagination-total="20" style="--paginate:true;--theme:cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme;">
 <h1>GeasOS におけるDPP実装(1/3)</h1>
 <ul>
 <li>5つのスレッドで並列処理を行う事で、哲学者の行動を再現する。</li>
@@ -228,7 +229,7 @@
 <li>par goto は複数スレッドでの実行であるので、各スレッドで実行後に__exitに継続する事で終了する。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="18" data-paginate="true" data-theme="za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj" data-marpit-pagination="18" data-marpit-pagination-total="20" style="--paginate:true;--theme:za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="18" data-paginate="true" data-theme="cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme" data-marpit-pagination="18" data-marpit-pagination-total="20" style="--paginate:true;--theme:cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme;">
 <h1>GearsOS におけるDPP実装(2/3)</h1>
 <ul>
 <li>マルチスレッドでのデータの一貫性を保証する手法としてCAS がある。</li>
@@ -237,22 +238,22 @@
 <li>DPPの例題ではフォークがスレッドで共有されるデータにあたるので、synchronixed Queue を用いることによってスレッド間での同期を行う。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="19" data-paginate="true" data-theme="za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj" data-marpit-pagination="19" data-marpit-pagination-total="20" style="--paginate:true;--theme:za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="19" data-paginate="true" data-theme="cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme" data-marpit-pagination="19" data-marpit-pagination-total="20" style="--paginate:true;--theme:cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme;">
 <h1>GearsOS におけるDPP実装(3/3)</h1>
+<p>v- 5つのスレッドで行われる処理の状態は6つあり、それぞれを状態変数で表す。</p>
 <ul>
-<li>5つのスレッドで行われる処理の状態は6つあり、それぞれを状態変数で表す。</li>
 <li>この状態遷移は goto next によって遷移し、metaCodeGear を 挟みメタレベルで各スレッドの状態を 各スレッドごとに用意した Memory Tree に保存する。</li>
 <li>Memory Tree はstateDBによってまとめられ、同じ状態は共有される。</li>
 <li>またDPPにおける状態遷移は無限ループであるため、stateDBを用いて同じ状態を検索することで、終了判定を行う。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="20" data-paginate="true" data-theme="za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj" data-marpit-pagination="20" data-marpit-pagination-total="20" style="--paginate:true;--theme:za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="20" data-paginate="true" data-theme="cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme" data-marpit-pagination="20" data-marpit-pagination-total="20" style="--paginate:true;--theme:cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme;">
 <h1>GearsOS でのモデル検査を実現する手法について</h1>
 <ul>
 <li>DPP をGearsOS 上のアプリケーションとして実装する。</li>
-<li>DPP codeGear のシャッフルの１つとして実行する。</li>
-<li>可能な実行を生成するiterator を作成する</li>
-<li>状態を記録するmemory Tree とstateDBを作成する。</li>
+<li>DPP を codeGear のシャッフルの１つとして実行する。</li>
+<li>可能な実行を生成する iterator を作成する</li>
+<li>状態を記録する memory Tree と stateDB を作成する。</li>
 </ul>
 </section>
 <script>!function(){"use strict";function t(t){Array.from(document.getElementsByTagName("svg"),e=>{if(e.hasAttribute("data-marpit-svg")){const{clientHeight:r,clientWidth:a}=e;e.style.transform||(e.style.transform="translateZ(0)");const o=t||e.currentScale||1,i=e.viewBox.baseVal.width/o,n=e.viewBox.baseVal.height/o,s=Math.min(r/n,a/i);Array.from(e.querySelectorAll(":scope > foreignObject"),t=>{const e=t.x.baseVal.value,o=t.y.baseVal.value;Array.from(t.querySelectorAll(":scope > section"),t=>{t.style.transformOrigin||(t.style.transformOrigin="0 0");const l=(a-s*i)/2-e,c=(r-s*n)/2-o;t.style.transform=`translate3d(${l}px,${c}px,0) scale(${s}) translate(${e}px,${o}px)`})})}})}const e=(t,e,r)=>{if(t.getAttribute(e)!==r)return t.setAttribute(e,r),!0};function r(a=!0){for(const e of"Apple Computer, Inc."===navigator.vendor?[t]:[])e();Array.from(document.querySelectorAll('svg[data-marp-fitting="svg"]'),t=>{const r=t.firstChild,a=r.firstChild,{scrollWidth:o,scrollHeight:i}=a;let n,s=1;if(t.hasAttribute("data-marp-fitting-code")&&(n=t.parentElement.parentElement),t.hasAttribute("data-marp-fitting-math")&&(n=t.parentElement),n){const t=getComputedStyle(n),e=Math.ceil(n.clientWidth-parseFloat(t.paddingLeft)-parseFloat(t.paddingRight));e&&(s=e)}const l=Math.max(o,s),c=Math.max(i,1),p=`0 0 ${l} ${c}`;e(r,"width",""+l),e(r,"height",""+c),e(t,"preserveAspectRatio",getComputedStyle(t).getPropertyValue("--preserve-aspect-ratio")||"xMinYMin meet"),e(t,"viewBox",p)&&t.classList.toggle("__reflow__")}),a&&window.requestAnimationFrame(()=>r(a))}!function(){if("undefined"==typeof window)throw new Error("Marp Core's browser script is valid only in browser context.");window.marpCoreBrowserScript?console.warn("Marp Core's browser script has already executed."):(Object.defineProperty(window,"marpCoreBrowserScript",{value:!0}),r())}()}();
--- a/presen/sigos.md	Thu May 28 01:39:29 2020 +0900
+++ b/presen/sigos.md	Thu May 28 09:06:39 2020 +0900
@@ -13,7 +13,7 @@
 
 - OS上ではさまざまなアプリケーションやサービスが提供されるが、予期しないエラーが起こり得る。
 - 本研究室で開発している GearsOS ではアプリケーションやサービスの信頼性をOSの機能として保証することを目指しており、今回はモデル検査による信頼性の保証について考察する。
-- またGearsOS そのものをGearsOS上でモデル検査することに関しても考察する。
+- またGearsOS そのものをGearsOS上でモデル検査する手法について考察する。
 ---
 
 # Gears OS
@@ -26,7 +26,7 @@
 
 # Continution based C
 
-- CbC とは C言語をベースとして、開発された言語でC言語との違いはプログラムにおける goto 文を用いて CodeGear　という単位で遷移する。
+- CbC とは C言語をベースとして、開発された言語でC言語との違いはプログラムにおける goto 文を用いて CodeGear という単位で遷移する。
 - goto 文による遷移は関数呼び出しとは異なり、stackや環境を隠して持つことがない。
 - 以下は CbC によって記述された codeGear です。
 ```
@@ -84,7 +84,7 @@
 
 ---
 
-# cotntextと状態数
+# contextと状態数
 
 - プログラムの非決定的な実行は、入力あるいは並列実行の非決定性から生じる。
 - 並列実行の非決定性は、同時に実行される codeGear の順列並び替えになるので、それらの並び替えを生成し、その際に生じるcontextの状態を数え上げる事で、モデル検査を実装できる。
@@ -104,12 +104,12 @@
 # モデル検査
 
 - モデルとは検証したいアプリケーションやサービスの振る舞いや性質を抽象化して表現したものであり、抽象化の手法には以下のようなものがある。
-- このモデルが仕様を満たしているかどうかを検査するものである。
 
  状態遷移モデル
  論理モデル
  組み合わせモデル
  フローモデル ..etc
+- このモデルが仕様を満たしているかどうかを検査するのがモデル検査である。
 - 検査の要点によってモデルを使い分ける必要性がある。
 
 ---
@@ -130,13 +130,13 @@
 ---
 
 # 既存のモデル検査手法(SPIN)
-
+- 一般的に扱われるモデル検査ツールとしてSPINがある。
 - SPIN はPromela (Process Meta Language)で記述される。
 - C言語と似た文法を持ち、元は通信プロトコルの検証として開発された言語であり、検証機を生成し、コンパイルと実行を行うことで検証される。
-- チャネルを使って通信や並列動作を記述する
+- チャネルを使って通信や並列動作を記述する。
 - 有限オートマトンに変換してモデル検査を行う。
 - Promelaへの書き換えが必要
-- SPIN では以下の性質を検査可能な性質
+- SPIN での検査可能な性質
  アサーション
  デッドロック
  到達性
@@ -150,8 +150,8 @@
 - Java Path Finder はjavaプログラムの検査ツール
 - java バーチャルマシン(JVM) を直接シュミレーション実行している、これによりjavaのバイトコードを直接実行可能である。
 - バイトコードを状態遷移モデルとして扱い、実行時に遷移し得る状態を網羅的に検査している。
-- 実行パターンを網羅的に調べるため、複数のプロセスの取り扱いができず、また状態空間が巨大な場合は、一部を抜き出して実行する必要がある。
-- JPF では以下の性質を検査することができる
+- 実行パターンを網羅的に調べるため、複数のプロセスの取り扱いができず、また状態空間が巨大な場合は、一部を抜き出して検査する必要がある。
+- JPF で検査可能な性質
  スレッドの可能な実行すべてを調べる
  デッドロックの検出
  アサーション
@@ -161,30 +161,30 @@
 
 # モデル検査手法について
 - GearsOS におけるモデル検査はcode gear 単位の順列組み合わせによって行われる。
-- codegear 実行後の状態を検査し、データベースに格納する。
-- 新しい上体が生成されなくなった時モデル検査が終了する。
+- codegear 実行後の状態を、データベースに格納する。
+- 新しい状態が生成されなくなった時モデル検査が終了する。
 - 哲学者５人が次の状態に進めなくなった時をデッドロックとして検出する。
 - 必要な状態はフォークの状態だけになるので、それ以外の状態は無視することができる。
 - これにより状態数を下げることができる。
 - つまり、問題に合わせたメタ計算により、モデル検査の状態数を下げることができる。
-- GearsOS による検証用プログラムとして Dining Philosohers Ploblem (以下DPP）を用いる。
+- GearsOS による検証用プログラムとして Dining Philosohers Ploblem (DPP）を用いる。
+
+---
+
+# DPP(dining philosohers ploblem)
+
+- 5人の哲学者が円卓についており、各々スパゲティーの皿が目の前に用意され、スパゲティーは絡まっている為２つのフォーク使わなければ食べれない。
+- フォークは皿の間に１本ずつの計5本しかないため、すべての哲学者が同時に食事することはできず、また全員がフォークを1本ずつ持ってしまった場合、誰も食事することは出来ない。この状態をデッドロックとする。
+<center><img src="./pic/dpp_image.svg" alt="" width="48%" height="48%" ></center>
 
 ---
 
 # DPP
 
-- 5人の哲学者が円卓についており、各々スパゲティーの皿が目の前に用意され、スパゲティーは絡まっている為２つのフォーク使わなければ食べれない。
-- フォークは席の間に１本ずつある。哲学者は、思考とフォークを持つ、食事する。
-<center><img src="./pic/dpp_image.svg" alt="" width="50%" height="50%" ></center>
-
----
-
-# DPP
-
-- 状態は以下の構成要素からなる
+- 状態の構成要素は次の6つからなる。
 `Pickup Right fork` ` Pickup Left fork` `eating` ` Put Right fork` `Put Left fork` ` Thinking `
 
-<bottom><img src="./pic/dpp_image.svg" alt="" width="70%" height="70%" ></bottom>
+<right><img src="./pic/dpp_image.svg" alt="" width="55%" height="55%" ></right>
 
 ---
 
@@ -200,27 +200,29 @@
 
 # GearsOS におけるDPP実装(2/3)
 
-- マルチスレッドでのデータの一貫性を保証する手法としてCAS がある。
-- CAS(Check and Set)を用いて実装されており、値の比較、更新をアトミックに行う。
+- マルチスレッドでのデータの一貫性を保証する手法としてCheck and Set (CAS) がある。
+- CAS を用いて値の比較、更新をアトミックに行う。
 - CAS は書き込みの際に、書き込む MetaCodeGear に更新前と更新後の値を渡し、更新前の値が保存されているメモリ番地の値と比較し同じデータがであれば書き込みを行う。異なる場合はほかからの書き込みがあったとみなし、値の更新に失敗し、もう一度CASを行う。
-- DPPの例題ではフォークがスレッドで共有されるデータにあたるので、synchronixed Queue を用いることによってスレッド間での同期を行う。
+- DPPの例題ではフォークがスレッドで共有されるデータにあたるので、CAS を用いることによってスレッド間での同期を行う。
 
 ---
 
 # GearsOS におけるDPP実装(3/3)
-- 5つのスレッドで行われる処理の状態は6つあり、それぞれを状態変数で表す。
+v- 5つのスレッドで行われる処理の状態は6つあり、それぞれを状態変数で表す。
 - この状態遷移は goto next によって遷移し、metaCodeGear を 挟みメタレベルで各スレッドの状態を 各スレッドごとに用意した Memory Tree に保存する。
 - Memory Tree はstateDBによってまとめられ、同じ状態は共有される。
 - またDPPにおける状態遷移は無限ループであるため、stateDBを用いて同じ状態を検索することで、終了判定を行う。
 
 ---
 
-# GearsOS でのモデル検査を実現する手法について
+# GearsOS でのモデル検査を実現する方法について
 - DPP をGearsOS 上のアプリケーションとして実装する。
-- DPP codeGear のシャッフルの１つとして実行する。
-- 可能な実行を生成するiterator を作成する
-- 状態を記録するmemory Tree とstateDBを作成する。
+- DPP を codeGear のシャッフルの１つとして実行する。
+- 可能な実行を生成する iterator を作成する
+- 状態を記録する memory Tree と stateDB を作成する。
 
 
 
 
+
+