Mercurial > hg > Members > atton > seminar_slides

annotate slides/20150519/slide.md @ 163:b8e16c48a5a4 default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update template
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Tue, 17 Jan 2017 17:18:41 +0900
parents 4c2f5cc9f676
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
104
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 title: Verification of programs using Code Segments and Data Segments
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 author: Yasutaka Higa
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 profile:
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 lang: Japanese
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 # 研究目的
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 * コードセグメントとデータセグメントという単位を用いてプログラムを記述する手法を提案する
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 * プログラムはコードセグメントという処理の集合として表され、相互に接続される
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 * 個々のコードセグメントを検証し、検証されたコードセグメントどうしの組み合わせによりプログラム全体を検証する
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 # 研究内容
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 * コードセグメントとデータセグメントを用いたプログラムに対し、自動で検証する機構を提案する
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 * 検証機構には可能な状態を列挙できるモデルチェッカーや、型システムを用いた証明を用いる
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 * 検証をメタ計算として定義し、通常のプログラムから検証を含んだプログラムを導出する
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 * メタ計算の形式化には Monad を用い、通常の計算とメタ計算間の一対一対応を保証する
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 # 近況報告
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 * Spin 触ってます
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 * チュートリアルとかちょろっと
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 # Spin
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 * Promela によって記述されたコードを実行するもの
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 * Promela は以下のような特徴を持つ
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 * proc という処理単位を並列に実行する
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 * boolean condition の assertion によって性質をチェックする
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 * proc の実行順を列挙することにより、反例などを見付ける
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 # Statements
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 * Promela の構文には2種類の状態がある(executable/blockng)
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 * 代入は always executable
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 * expression は non-zero の時のみ executable
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 * flag == 1 と書くと flag が 1 になるまで blocking
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 # control flow
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 * if によって実行を分岐できる
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 ```
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 if
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 :: condition -> expression
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 :: condition -> expression
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 ...
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 fi
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 ```
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 * condition が executable なものから non-deterministic に実行される
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 # repeat
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 * do 構文で if を repeat できる
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 ```
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 do
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 :: condition -> expression
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 :: condition -> expression
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 ...
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 od
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 ```
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 # assertion
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 * assert 構文で boolean の assertion ができます
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 * assert 構文は always executable
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 # channel
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 * proc 間の messaging
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 * ほとんど synchironized queue
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 * FIFO
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 * block when take from empty queue
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 * block when put to full queue
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 * golang の channel っぽい。
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 # 実装周りの話
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 * 状態は vector にしてるっぽいです
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 * 同じ vector は hash に入れてる
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76 # bibliographies
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 * [Spin Online References](http://spinroot.com/spin/Man/)
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 * [Tutorial](http://spinroot.com/spin/Doc/SpinTutorial.pdf)
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 * [Basic Spin Manual](http://spinroot.com/spin/Man/Manual.html)
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80
4c2f5cc9f676 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 <!-- vim: set filetype=markdown.slide: -->