Mercurial > hg > Members > atton > seminar_slides

comparison slides/20151215/slide.md @ 119:9f874edd19a4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add slide for seminar
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 15 Dec 2015 18:35:10 +0900
parents
children
comparison
equal deleted inserted replaced
118:9c9ba490943b 119:9f874edd19a4
1 title: Verification of programs using Code Segments and Data Segments
2 author: Yasutaka Higa
3 profile:
4 lang: Japanese
5
6
7 # 研究目的
8 * コードセグメントとデータセグメントという単位を用いてプログラムを記述する手法を提案する
9 * プログラムはコードセグメントという処理の集合として表され、相互に接続される
10 * 個々のコードセグメントを検証し、検証されたコードセグメントどうしの組み合わせによりプログラム全体を検証する
11
12 # 研究内容
13 * コードセグメントとデータセグメントを用いたプログラムに対し、自動で検証する機構を提案する
14 * 検証機構には可能な状態を列挙できるモデルチェッカーや、型システムを用いた証明を用いる
15 * 検証をメタ計算として定義し、通常のプログラムから検証を含んだプログラムを導出する
16 * メタ計算の形式化には Monad を用い、通常の計算とメタ計算間の一対一対応を保証する
17
18 # 近況報告
19 * Overview: Principles of Model Checker(1-8)
20 * Liner Temporal Logic
21 * Computation Tree Logic
22
23 # Overview: Principles of Model Checker
24 * 1: System Verification
25 * 2: Modeling Concurrent Systems
26 * 3: Liner-Time Properties
27 * 4: Regular Properties
28 * 5: Liner Temporal Logic
29 * 6: Computation Tree Logic
30 * 7: Equivalences and Abstraction
31 * 8: Partial Order Reduction
32
33 # 1: System Verification
34 * そもそもシステムを検証するとは何なのか的なお話
35 * Hardware/Software Verification Verification
36 * 仕様を命題として記述してシステムのモデルが命題を満たすかチェック
37 * 満たす/満たさない
38 * 満たさないなら反例を提出
39
40 # 2: Modeling Concurrent Systems
41 * System は Transition System として表わされる
42 * TS = (S, Act, ->, I, AP, L)
43 * S is Set of States
44 * Act is Set of Actions
45 * -> is transition relation ( S x Act x S )
46 * AP is set of atomic proposition
47 * L is labeling function (S -> 2^{AP})
48
49 # Figure: Transition System
50 * Vending Machine
51 ![TS](http://i.stack.imgur.com/bgJM8.png)
52
53 # 2: Modeling Concurrent Systems
54 * Concurrent System は transition system の相互接続として表現
55 * Shared Variable や Channel によって接続される
56 * Channel は容量の上限が決まった Message Queue
57 * Spin とかは Channel Connected Process として System を表現
58 * Promela (Process Meta Language) を使って書く
59
60 # 3: Liner-Time Properties
61 * 満たすべき命題をどうやって判断するか
62 * TS の遷移の path ら命題が満たされるか判断できる
63 * 例えば無限に動くシステムでも、命題を満たさない path-prefix があればダメ
64
65 # 4: Regular Properties
66 * 具体的にどのように検証するか
67 * Automaton に変換してしまえば良い
68 * Nondeterministic Finite Automaton とか
69 * ω-Regular Language
70
71 # 5: Liner Temporal Logic
72 * 命題をどのように記述するか
73 * Liner Temporal Logic
74 * ``φ ::= true | a | φ1 ∩ φ2 | ¬ φ | ○φ | φ1 U φ2``
75 * ○は next
76 * U は until。 right-operand を満たすまで left-operand は true である
77
78 # 5: Liner Temporal Logic
79 * 信号は赤になる時がある
80 * eventually ◇ == true U φ
81 * eventually red
82 * true U red
83 * 信号は赤か青か黄色である
84 * always □ == not eventually not φ
85 * always (red or green or yellow)
86 * not (eventually (not (red or green or yellow)))
87
88 # 5: Liner Temporal Logic
89 * 検証は automaton とセットで。
90 * 無限に生成される言語の受理状態をチェックできるω-Automaton もある
91 * NBA (Nondeterministic Buchi Automata) を使って infinite transition system の検証も
92
93 # 6: Computation Tree Logic
94 * 命題の別の記述方法
95 * transition を tree にしてチェック
96 * `` state formula : Φ ::= true | Φ1 ∧ Φ2 | ¬Φ | ∃φ | ∀φ ``
97 * `` path formula : φ ::= ○Φ | Φ1 U Φ2 ``
98 * eventually/always もあります
99
100 # 7: Equivalences and Abstraction
101 * Equivalences な TS を検証することでサイズを小さくしよう
102 * Bisimulation とか
103 * 一部置き換えたシステムとかもあるみたいです
104
105 # 8: Partial Order Reduction
106 * 並列に実行した再に順番が変わっても大丈夫なやつをまとめてサイズを小さくしよう
107 * Ample Set とか
108 * この辺から最適化っぽかったのでとりあえず一旦読むのを中断
109
110 # 現状検証するべき condition
111 * おそらく一番安直には
112 * always balanced
113 * insertion/deletion 途中は回転とかするはずなので
114 * always (balancing or balanced)
115 * これで必要十分?
116
117 # 命題の記述に何を採用するか
118 * CTL のが簡単そうなのでまずはこれでやろうかと
119 * bounded になるはず
120 * insertion/deletion の operation 列が有限
121
122 # CbC をどうやって Transition System に変更にするか
123 * goto を transition にすれば簡単
124 * next は次の state
125 * conditional な Transition System をどうするか
126 * condition を覚えておいて SAT する
127 * でいけそうな気はしてます
128
129 # 課題
130 * このやり方だとメタ計算でやるよりも CbC を直接パースした方が簡単そう
131 * SAT が必要なので condition 覚えるのと SAT の実装が
132
133
134 <!-- vim: set filetype=markdown.slide: -->