title: Verification of programs using Code Segments and Data Segments
author: Yasutaka Higa
profile:
lang: Japanese


# 研究目的
* コードセグメントとデータセグメントという単位を用いてプログラムを記述する手法を提案する
* プログラムはコードセグメントという処理の集合として表され、相互に接続される
* 個々のコードセグメントを検証し、検証されたコードセグメントどうしの組み合わせによりプログラム全体を検証する

# 研究内容
* コードセグメントとデータセグメントを用いたプログラムに対し、自動で検証する機構を提案する
* 検証機構には可能な状態を列挙できるモデルチェッカーや、型システムを用いた証明を用いる
* 検証をメタ計算として定義し、通常のプログラムから検証を含んだプログラムを導出する
* メタ計算の形式化には Monad を用い、通常の計算とメタ計算間の一対一対応を保証する

# 近況報告
* Overview: Principles of Model Checker(1-8)
* Liner Temporal Logic
* Computation Tree Logic

# Overview: Principles of Model Checker
* 1: System Verification
* 2: Modeling Concurrent Systems
* 3: Liner-Time Properties
* 4: Regular Properties
* 5: Liner Temporal Logic
* 6: Computation Tree Logic
* 7: Equivalences and Abstraction
* 8: Partial Order Reduction

# 1: System Verification
* そもそもシステムを検証するとは何なのか的なお話
* Hardware/Software Verification Verification
* 仕様を命題として記述してシステムのモデルが命題を満たすかチェック
    * 満たす/満たさない
    * 満たさないなら反例を提出

# 2: Modeling Concurrent Systems
* System は Transition System として表わされる
* TS = (S, Act, ->, I, AP, L)
    * S is Set of States
    * Act is Set of Actions
    * -> is transition relation ( S x Act x S )
    * AP is set of atomic proposition
    * L is labeling function (S -> 2^{AP})

# Figure: Transition System
* Vending Machine
![TS](http://i.stack.imgur.com/bgJM8.png)

# 2: Modeling Concurrent Systems
* Concurrent System は transition system の相互接続として表現
* Shared Variable や Channel によって接続される
* Channel は容量の上限が決まった Message  Queue
    * Spin とかは Channel Connected Process として System を表現
    * Promela (Process Meta Language) を使って書く

# 3: Liner-Time Properties
* 満たすべき命題をどうやって判断するか
* TS の遷移の path ら命題が満たされるか判断できる
* 例えば無限に動くシステムでも、命題を満たさない path-prefix があればダメ

# 4: Regular Properties
* 具体的にどのように検証するか
* Automaton に変換してしまえば良い
    * Nondeterministic Finite Automaton とか
* ω-Regular Language

# 5: Liner Temporal Logic
* 命題をどのように記述するか
* Liner Temporal Logic
    * ``φ ::= true | a | φ1 ∩ φ2 | ¬ φ | ○φ | φ1 U φ2``
* ○は next
* U は until。 right-operand を満たすまで left-operand は true である

# 5: Liner Temporal Logic
* 信号は赤になる時がある
    * eventually ◇ == true U φ
    * eventually red
    * true U red
* 信号は赤か青か黄色である
    * always □ == not eventually not φ
    * always (red or green or yellow)
    * not (eventually (not (red or green or yellow)))

# 5: Liner Temporal Logic
* 検証は automaton とセットで。
* 無限に生成される言語の受理状態をチェックできるω-Automaton もある
* NBA (Nondeterministic Buchi Automata) を使って infinite transition system の検証も

# 6: Computation Tree Logic
* 命題の別の記述方法
* transition を tree にしてチェック
    * `` state formula : Φ  ::= true | Φ1 ∧ Φ2 | ¬Φ | ∃φ | ∀φ ``
    * `` path formula  : φ  ::= ○Φ | Φ1 U Φ2 ``
* eventually/always もあります

# 7: Equivalences and Abstraction
* Equivalences な TS を検証することでサイズを小さくしよう
    * Bisimulation とか
    * 一部置き換えたシステムとかもあるみたいです

# 8: Partial Order Reduction
* 並列に実行した再に順番が変わっても大丈夫なやつをまとめてサイズを小さくしよう
* Ample Set とか
* この辺から最適化っぽかったのでとりあえず一旦読むのを中断

# 現状検証するべき condition
* おそらく一番安直には
    * always balanced
* insertion/deletion 途中は回転とかするはずなので
    * always (balancing or balanced)
* これで必要十分?

# 命題の記述に何を採用するか
* CTL のが簡単そうなのでまずはこれでやろうかと
    * bounded になるはず
    * insertion/deletion の operation 列が有限

# CbC をどうやって Transition System に変更にするか
* goto を transition にすれば簡単
    * next は次の state
* conditional な Transition System をどうするか
    * condition を覚えておいて SAT する
    * でいけそうな気はしてます

# 課題
* このやり方だとメタ計算でやるよりも CbC を直接パースした方が簡単そう
    * SAT が必要なので condition 覚えるのと SAT の実装が


<!-- vim: set filetype=markdown.slide: -->