Model Checking Ch.2

MC Ch.2: Introduction to the first edition #

プログラム解析技術の俯瞰(ISA より):

自動？健全？完全？対象動的・静的
TestingYesNoYesProgram動的
Assisted provingNoYesYes/NoModel静的
Model checking of
finite-state model		YesYesYesFinite
model		静的
Model checking at
program level		YesYesNoProgram静的
Conservative static
analysis		YesYesNoProgram静的
Bug findingYesNoNoProgram静的

Model checking (MC):

  • 自動
    • 人間の介入が必要な技術もある (→ Assisted proving)
      • e.g. Coq など自動定理証明技術は、プログラムの意味論などを人間が入力として与える必要あり
  • 回路の設計や通信プロトコルの検証に使われている

MC における課題と近年の発展:

  • 課題: 状態爆発
    • 数多くのコンポーネントが絡みあったりすると、考慮すべき状態の数は指数的に増える
  • 近年の発展: 状態爆発を抑える技術は 10 年で飛躍的に進歩した

この章で何をみるか:

  • MC とその他の形式的検証技術の比較
    • 特に、SW/HW の設計に関する検証について
  • MC アルゴリズム間の比較
    • 状態爆発への対処の比較

The Need for Formal Methods #

SW/HW はミッションクリティカルな場面で使われている。例えば…:

  • 航空管制
  • ロケット制御
  • 医療関連のシステム
  • 通販
  • …

SW/HW が原因による事故が度々起きている:

  • 最も有名なのは「1996 年: アリアン 5 ロケットが打ち上げ後 40 秒で爆発」
    • 爆破までの流れ:
      1. 64 bit の浮動小数が 16bit の signed int に変換
      2. 例外発生
      3. 2.の例外がキャッチされずコンピュータがクラッシュ
      4. バックアップコンピュータも同様にクラッシュ
      5. 誤った高度データが基板コンピュータ（？）に送られ、結果的に爆破
    • 被害:
      • ロケット＋積荷：5 億ドル
      • 10 年の開発費用：70 億ドル
    • 参照 1:クラスターミッション
    • 事故映像

SW/HW の正しさを証明する技術は近年ますます重要になってきている！:

  • 我々はミッションクリティカルなシステムに囲まれている。
  • 「おかしくなったら電源を落とせばいい」のような単純な話では無い。(例：飛行機)
  • 技術は急速に発展している。
    • → 正しさを証明する技術の重要性

Hardware and Software Verification #

Validation methods (順に見る):

  • simulation
  • testing
  • =====
  • deductive verification
  • model checking

Simulation and Testing:

  • いつ？
    • デプロイ前に実験を行う
  • 何に対して？
    • simulation : モデルの上などで行われる
      • e.g. 回路の設計に対して行われる
    • testing : 実際のプロダクトで行われる
      • e.g. 実際の回路に対して行われる
  • どのように？
    • 特定の入力に対する出力を観測する
  • しかし…
    • 全てのパターンを網羅するのはほぼ不可能!
    • バグの見逃しが発生してしまう orz
      • 人が死ぬぞ？

Deductive verification とは:

  • 公理 (axioms) と証明規則を用いてシステムの正しさを証明する
  • 欠点:
    • 人の介入が必要
      • 数学者, 記号論理学に精通した人,…
  • 利点:
    • 無限状態のシステムを扱える
      • しかし、証明の発見に必要なリソースの上限は無い。
        • バカ食いする可能性あり。

Model checking とは:

  • 有限状態の並列システムを検査する
  • 欠点:
    • 有限状態しか扱えない
  • 利点:
    • 検査を自動で行える
    • 検査は必ず終わる
      • しかも、yes/no の答えを必ず出す
    • 効率的なアルゴリズムが存在する
      • 普通の PC でも動く

Model checking (cont.):

  • 無限状態は扱えないが、以下の超大事なシステム群を扱える:
    • HW controllers
    • 通信プロトコル
  • 場合によっては、無限システムも扱える
    • MC 以外の手法の組み合わせ
  • 入力を制限することで、システムを有限状態システムに落とせる

結論: Model Checking を使えるなら使え。必要な時のみ Deductive Verification を。

The Process of Model Checking #

以下では Model Checking を MC と書く。

①: Modeling

  • Model checker が読める形に設計・プログラムを変換する（一種のコンパイル）
    • Kripke structure (後述)
  • 必要に応じて抽象化も行う
    • → 時間・メモリ量を削減できる

②: Specification (仕様)

  • システムに満たして欲しい性質を論理形式に変換する
    • Temporal logic
  • 仕様が、上記の性質をカバーしているか注意する必要あり
    • 「システムが仕様を満たす」と言われても、
      仕様が性質を正しく表現してなければ意味がない

③: Verification

  • 基本的には全て自動
    • ただし、結果の解釈は人力
  • ④ のトレースの用途:
    • システムの解析（見直し）
    • ① の Modeling の修正
    • ② の Specification の修正

Temporal Logic and Model Checking #

Temporal logic: 時相論理

時相論理:

  • 時間を明示的に扱うことなく（システムの）イベントの順序を表現できる論理
    • 並列システムには最適
  • よく出る形:
    • $\mathbf{G}f$ : $f$ が将来ずっと (globally) 成立する時、真になる。
    • e.g. $\mathbf{G}(\lnot e_1 \lor \lnot e_2)$ : イベント $e_1$ と $e_2$ は同時には必ず起きない
  • 時間に対する仮定は 2 通りある (後の章で出てくる):
    1. Linear structure
    2. Branching structure

時相論理の用途（の歴史）:

  • プログラムへの適用 (Burstall (1974), Kroger (1977), Pnueli (1977))
  • 特に、並列システムへの適用 (Pnueli (1977))
  • シーケンス回路への適用 (Bochmann (1982), Malachi et al. (1981))
  • 時相論理を用いたモデル検査 (Clarke et al. (1981))
    • 初めてモデル検査が自動化される。
      • Branching-time temporal logic (CTL, 後の章で出てくる) での検査
    • モデルのサイズ、仕様の長さに関して多項式時間のアルゴリズム
    • 正当性 (fairness, 後の章で出てくる) も扱える
      • e.g. 飢餓の不在の証明を行うには正当性を扱う必要あり
  • CTL の部分集合に対するモデル検査 (Queille et al. (1982)) (メモ：どういう部分集合なのか？)
    • 論理式の長さ * 状態遷移グラフのサイズ に対して線形なアルゴリズム (Clarke et al. (1986))
    • $10^4 \sim 10^5$ 程度の状態数を扱える（$100$ 状態/秒）
    • ネットワークプロトコル、シーケンス回路の検査で広く使われた。

時相論理の用途（の歴史）2:

  • Linear Time Logic (LTL) に対するモデル検査:
    • PSPACE-complete (Sistla et al. (1983, 1985))
    • 計算量:
      • 仕様の論理式のサイズに対しては指数オーダーだが
      • 大域状態グラフのサイズに対しては線形 (Pnueli et al. (1985))
        → 短い仕様に関しては十分に検査可能
  • CTL* (=CTL (branching-time) + LTL (linear-time)) に対するモデル検査:
    • PSPACE-complete (Clarke et al. (1983))
    • LTL に対するモデル検査と同様の計算量のアルゴリズムが示される (Emerson et al. (1985))
      • 仕様を LTL に制限する意味はない

Symbolic Algorithms #

  • モデル検査の実装において、遷移関係は隣接リストで表現されていた
    • プロセス数：少 → 十分に扱える
    • プロセス数：多 → 状態遷移グラフ：大、扱いきれない
  • 記号表現を用いて状態遷移グラフを扱えば、より大きなシステムの検査が可能になるのでは？(McMillan (1987))
  • OBDDs: Ordered Binary Decision Diagrams (Bryant (1986))
    • 非常に小さい形式で論理式を表現できる (ref: canonical form)
    • 効率の良いアルゴリズムも存在する
  • 扱える状態数が桁違い
    • 状態空間の規則 (regularity) を捉える。
    • 状態を明示的に扱うアルゴリズムより何桁も多い状態数を扱える。
  • e.g.:
    • CTL のモデル検査において記号表現を用いた場合: $10^{20}$ 程度の状態数を扱える (Burch et al. (1990))
    • OBDD ベースの技術: $10^{120}$ 程度の状態数を扱える (Burch et al. (1991, 1994))

Partial Order Reduction #

SW: Software
HW: Hardware

SW の検査では状態爆発が問題になる:

  • 並列プログラムはしばしば非同期的な挙動を見せるため。
  • 従って、SW での検査は HW ほどは行われていない。

SW の検査での状態爆発に対処する技術が発展している:

  • その中でも最も成功しているのが、partial order reduction
    • (Godefroid et al. (1993), Peled (1994), Valmari (1990))
    • 大域状態 (global state) が同じになるような interleaving を 1 つにまとめる。
  • この本では ample sets と呼ばれるモデル検査の手法を 12 章で扱う。
Partial Order Reduction による探索空間の削減

独立なイベント:

  • 2 つのイベントは次の時独立
    • 実行する順番を入れ替えても最終的な大域状態 (global state) が同じ

独立なイベント $e_1, e_2, e_3$ があった時、以下のようにモデル検査での探索空間を削減できる:

Other Approaches to the State Explosion Problem #

その他手法（列挙に留めておく）:

  • Compositional reasoning
  • Abstraction
  • Symmetry
  • Induction

まとめとクイズ #

  • Q1. モデル検査の流れを述べよ
  • Q2. モデル検査における課題は？
  • Q3. Q2 での課題を克服するアイデアを述べよ
Calendar Jul 4, 2023