Mercurial > hg > Papers > 2018 > nozomi-master

diff presentation/slide.html @ 121:137aae675a94

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update slide
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Tue, 14 Feb 2017 15:03:04 +0900
parents 8a84cda440f3
children c195713cf7d7
line wrap: on
line diff
--- a/presentation/slide.html	Tue Feb 14 11:31:08 2017 +0900
+++ b/presentation/slide.html	Tue Feb 14 15:03:04 2017 +0900
@@ -86,7 +86,7 @@
 <!-- === begin markdown block ===
 
       generated by markdown/1.2.0 on Ruby 2.3.3 (2016-11-21) [x86_64-darwin16]
-                on 2017-02-14 11:30:47 +0900 with Markdown engine kramdown (1.13.0)
+                on 2017-02-14 15:02:42 +0900 with Markdown engine kramdown (1.13.0)
                   using options {}
   -->
 
@@ -146,6 +146,7 @@
 <!-- _S9SLIDE_ -->
 <h1 id="section-3">モデル検査的アプローチについての流れ</h1>
 <ul>
+  <li>既存のモデル検査器について</li>
   <li>Continuation based C (CbC) 言語について</li>
   <li>CbC における CodeSegment と DataSegment を用いたプログラミングスタイル</li>
   <li>CbC とメタ計算について</li>
@@ -157,13 +158,60 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
+<h1 id="spin">既存のモデル検査器 spin</h1>
+<ul>
+  <li>spin
+    <ul>
+      <li>promela と呼ばれる言語でプログラムを記述</li>
+      <li>並列に動作するプログラムの仕様を検証可能</li>
+      <li>検証した promela から実行可能な C ソースを生成可能</li>
+      <li>仕様は bool になる式を用いた assert</li>
+      <li>デメリット: promela は C とは記述が異なる</li>
+    </ul>
+  </li>
+</ul>
+
+<pre><code>assert(x &lt; 10);
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="cbmc">既存のモデル検査器 CBMC</h1>
+<ul>
+  <li>CBMC
+    <ul>
+      <li>検証対象のCソースを変更しないでも良い</li>
+      <li>C/C++ 言語の記号実行が可能
+        <ul>
+          <li>条件分岐を網羅的に実行</li>
+        </ul>
+      </li>
+      <li>仕様は bool になる式を用いた assert</li>
+      <li>有限ステップだけ検証する有界モデル検査器</li>
+    </ul>
+  </li>
+</ul>
+
+<pre><code>assert(x &lt; 10);
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
 <h1 id="continuation-based-c">Continuation based C</h1>
 <ul>
   <li>当研究室で開発しているプログラミング言語</li>
   <li>アセンブラとC言語の中間のような言語であり、構文はほとんど C 言語</li>
   <li>OS や組み込みソフトウェアなどを対象にしている</li>
   <li>CodeSegment と DataSegment という単位を用いてプログラミングする</li>
-  <li>両検証手法をメタ計算として利用可能</li>
+  <li>モデル検査と証明の両検証手法をメタ計算として利用可能
+    <ul>
+      <li>CbC で CbC 自身を検証可能</li>
+    </ul>
+  </li>
 </ul>
 
 
@@ -242,7 +290,7 @@
   <li>通常の CodeSegment どうしの接続の間に入る</li>
 </ul>
 
-<p><img src="./images/mcs.svg" alt="mcs" width="50%" /></p>
+<p><img src="./images/mcs.svg" alt="mcs" width="75%" /></p>
 
 
 </div>
@@ -254,7 +302,7 @@
   <li>通常の DataSegment を含むような DataSegment</li>
 </ul>
 
-<p><img src="./images/mds.svg" alt="mds" width="50%" /></p>
+<p><img src="./images/mds.svg" alt="mds" width="75%" /></p>
 
 
 </div>
@@ -294,7 +342,6 @@
 <ul>
   <li>挿入したい要素を DataSegment に格納して次の CodeSegment へ goto</li>
   <li>goto する前に Meta CodeSegment が実行されて木に挿入する</li>
-  <li>GearsOS では木の実装のためにスタックを用いて経路情報を保持している</li>
 </ul>
 
 <p><img src="./images/put.svg" alt="put" width="50%" /></p>
@@ -310,7 +357,7 @@
 <ul>
   <li>「バランスが取れている」とは何かを表現できる必要がある
     <ul>
-      <li>実行可能な CbC の式を使った assert になる</li>
+      <li>実行可能な CbC の条件式を使った assert になる</li>
     </ul>
   </li>
   <li>そしてそれを保証したい
@@ -324,49 +371,6 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="spin">既存のモデル検査器 spin</h1>
-<ul>
-  <li>spin
-    <ul>
-      <li>promela と呼ばれる言語でプログラムを記述</li>
-      <li>並列に動作するプログラムの仕様を検証可能</li>
-      <li>検証した promela から実行可能な C ソースを生成可能</li>
-      <li>仕様は bool になる式を用いた assert</li>
-      <li>デメリット: promela は C とは記述が異なる</li>
-    </ul>
-  </li>
-</ul>
-
-<pre><code>assert(x &lt; 10);
-</code></pre>
-
-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h1 id="cbmc">既存のモデル検査器 CBMC</h1>
-<ul>
-  <li>CBMC
-    <ul>
-      <li>検証対象のCソースを変更しないでも良い</li>
-      <li>C/C++ 言語の記号実行が可能
-        <ul>
-          <li>条件分岐を網羅的に実行</li>
-        </ul>
-      </li>
-      <li>仕様は bool になる式を用いた assert</li>
-      <li>有限ステップ検証する有界モデル検査器</li>
-    </ul>
-  </li>
-</ul>
-
-<pre><code>assert(x &lt; 10);
-</code></pre>
-
-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
 <h1 id="section-7">チェックする仕様</h1>
 <ul>
   <li>赤黒木の高さに関する仕様に以下のものがある
@@ -407,7 +411,7 @@
   <li>ノーマルレベルのコードを検証用に変更せず検証可能</li>
 </ul>
 
-<p><img src="./images/akashaPut.svg" alt="akashaPut" width="51%" /></p>
+<p><img src="./images/akashaPut.svg" alt="akashaPut" width="50%" /></p>
 
 
 </div>
@@ -438,7 +442,7 @@
 <h1 id="continuation-based-c-">定理証明を Continuation based C へ適用するには</h1>
 <ul>
   <li>任意の回数だけ木の操作を行なっても大丈夫なことを保証したい</li>
-  <li>そのままプログラムの性質を保証してやる</li>
+  <li>直接プログラムの性質を証明</li>
   <li>Coq, Agda, ATS2 などのプログラミング言語で証明が可能
     <ul>
       <li>本当は CbC で CbC 自身を証明したい</li>
@@ -454,7 +458,11 @@
 <!-- _S9SLIDE_ -->
 <h1 id="agda--datasegment">Agda と DataSegment</h1>
 <ul>
-  <li>CbC の DataSegment は Agda のレコード型</li>
+  <li>CbC の DataSegment は Agda のレコード型
+    <ul>
+      <li>名前付きの値が複数ある(C の構造体)</li>
+    </ul>
+  </li>
 </ul>
 
 <pre><code>__code cs0(int a, int b){
@@ -473,7 +481,11 @@
 <!-- _S9SLIDE_ -->
 <h1 id="agda--codesegment">Agda と CodeSegment</h1>
 <ul>
-  <li>CbC の CodeSegment は、Agda の関数型(Input を取って Output を返す)</li>
+  <li>CbC の CodeSegment は、Agda の関数型
+    <ul>
+      <li>Input を取って Output を返す</li>
+    </ul>
+  </li>
 </ul>
 
 <pre><code>__code cs0(int a, int b){
@@ -580,10 +592,11 @@
 <!-- _S9SLIDE_ -->
 <h1 id="section-10">今後の課題</h1>
 <ul>
+  <li>より大きなサイズの赤黒木の検証</li>
+  <li>赤黒木の挿入に関する性質を証明する</li>
   <li>部分型を利用してCbCを型付け</li>
   <li>依存型をCbC に導入して自身を証明可能にする</li>
   <li>型情報から stub を自動生成すkる</li>
-  <li>赤黒木の挿入に関する性質を証明する</li>
 </ul>