モデル検査（１） 並行システムとモデル検査 １．並行システム ２．モデル検査 ３．モデル検査の実施 ４．システムとアルゴリズム 表現系工学特論 (model checking) モデル検査（１） 並行システムとモデル検査 (concurrent systems and model checking) １．並行システム ２．モデル検査 ３．モデル検査の実施 ４．システムとアルゴリズム 参考文献 Model Checking, E.M. Clarke, Jr. et al, MIT Press (1999)

並行システム プロセス間通信 インタリーブ 相互排他 デッドロック ライブロック，飢餓 １．並行システム (concurrent systems) 並行システム プロセス間通信 インタリーブ 相互排他 デッドロック ライブロック，飢餓 (concurrent systems) (inter-process communication) (interleave) (mutual exclusion) (deadlock) (livelock, starvation)

並行システム(1/7) リアクティブ･システム（reactive system） (concurrent systems) 複数のプロセス(process)が並列(または擬似並列)に動作する計算システム リアクティブ･システム（reactive system） 環境からのイベント(event)の入力に実時間(real-time)的に応答する並行システム

並行システム(2/7) 非同期・交互実行 一度に1つのコンポーネントだけが、1ステップ処理を進める 同期実行 実行方法 非同期・交互実行 一度に1つのコンポーネントだけが、1ステップ処理を進める (asynchronous, interleaved) 同期実行 同時に全てのコンポーネントが、1ステップ処理を進める (synchronous)

並行システム(3/7) 共有変数 非同期メッセージ通信（キューを用いる） 同期メッセージ通信（ハンドシェイク） プロセス間の通信方法 (shared variable) 非同期メッセージ通信（キューを用いる） (asynchronous message passing with a queue) 同期メッセージ通信（ハンドシェイク） (synchronous message passing, handshaking)

並行システム(4/7) インタリーブ (interleave) a Process Ａ b Process Ｂ b a インターリーブは 予期できない(unpredictable) 制御できない(uncontrollable) 膨大な数の実行経路を生じる (a huge number of paths)

並行システム(5/7) 相互排他 (mutual exclusion) 共有変数は相互排他が必要 m = m + 1000; Process Ａ m = m + 1000; Shared var ｍ=5000 Process B m = m - 1000; MOV A,m (A=5000) 1 ADD A,1000 (A=6000) 2 3 MOV B,m (B=5000) 4 SUB B,1000 (B=4000) MOV m,A (m=6000) 5 6 MOV m,B (m=4000)

30万円の口座に10万円を送る BANK 300000 400000 300000 400000 300000 400000 300000 400000 300000 300000 400000

預入れと引出しが ほぼ同時の場合 deposit and withdrawal almost at the same time BANK 30万円の口座に10万円を送る deposit and withdrawal almost at the same time BANK 200000 300000 200000 300000 200000 400000 300000 300000 400000 300000 400000

並行システム(6/7) デッドロック (deadlock) acquire Scanner acquire Printer Process　Ａ Scanner Process　Ｂ Printer acquire Scanner 1 acquire Printer 2 DEADLOCK acquire Printer acquire Printer acquire Scanner acquire Scanner acquire Scanner Copy Copy

並行システム(7/7) ライブロック，飢餓 (livelock) (starvation) request request request Resource Process　Ａ (lower preference) 優先順位が低い Process　Ｂ Process　C request request request acquire acquire (no fairness) request 公平性がない acquire Printer acquire request acquire Scanner acquire Scanner プロセスＣは決して資源を獲得できない acquire (Process C can never acquire the resource)

モデル検査とは何か 有限状態システム 検証できる性質 ２．モデル検査 (model checking) モデル検査とは何か 有限状態システム 検証できる性質 (What is the model checking) (Finite state systems) (Verifiable properties)

モデル検査とは何か 有限状態並行システム の検証を自動で行う技術 並行システム 複数のプロセスが並列(または擬似並列)に動作 (model checking) 有限状態並行システム の検証を自動で行う技術 並行システム 複数のプロセスが並列(または擬似並列)に動作 有限状態システム 状態数が有限個の状態遷移系 検証 期待される性質(仕様)を満たすことの確認 (finite state concurrent systems) (verification) (concurrent systems) (finite state systems) (verification) (confirm the expected property or specification)

(primitive propositions) 状態遷移系（オートマトン） (state transition system; automaton) event label (primitive propositions) ４-counter 1 1 q p tick initial state tick p tick q tick p,q reset reset state 1 state 2 state 3 state 0 reset reset 状態（ノード）の有限集合 初期状態の集合 遷移関係（辺の集合） 各状態ごとのラベル 状態数は数百万くらいはＯＫ (millions of states OK in practice)

検証できる性質(1/3) 安全性 (safety) 「悪いことは決して起こらない」という性質 ＝「良いことは常に成り立つ」 (Verifiable properties) 安全性 (safety) 　　「悪いことは決して起こらない」という性質 　　＝「良いことは常に成り立つ」 活性(liveness) 　　「良いことはいつかは成り立つ」という性質 (The bad thing will never happen) (The good thing will eventually happen) なにが「悪いこと」で，なにが「良いこと」かは，応用目的にあわせて設計者が記述する

検証できる性質(2/3) 安全性： 「悪いことは決して起こらない」 決してデッドロックしない 安全性：　「悪いことは決して起こらない」 決してデッドロックしない このエレベータは，ドアが開いたまま昇降することは決してない このメッセージは，暗号化されずに送信されることは決してない

検証できる性質(3/3) 活性: 「良いことはいつか必ず起こる」 資源を要求したら，いつか必ず取得できる 活性:　「良いことはいつか必ず起こる」 資源を要求したら，いつか必ず取得できる ＯＫボタンを押すと，いつか必ず動作する このメッセージは必ず宛先に届く

ソフトウェアのライフサイクル： When & Who モデル検査の実施手順： How 他の検証法： Why ３．モデル検査の実施 (conducting model checking) ソフトウェアのライフサイクル：　When & Who モデル検査の実施手順：　How 他の検証法：　Why

ソフトウェアのライフサイクル： When & Who ソフトウェア開発の上流工程で設計者が実施 モデリング 分析 仕様書 analysis modeling 設計 設計書 design 実装 コード implement テスト software lifecycle (waterfall model) test 製品 運用 operation

モデル検査の実施手順： How (1)モデリング (2)性質の記述 (3)検証 (develop a model) (describe desired properties) (3)検証 (verify; model check)

(1) モデリング 設計をモデル記述言語で記述し， モデル（状態遷移系）を定義する C言語風の言語 SPIN (Promela言語） (model description language) 設計をモデル記述言語で記述し， モデル（状態遷移系）を定義する モデル記述言語 C言語風の言語 SPIN (Promela言語） SMV, NuSMV プロセス代数に基づく言語 LTSA (FSP)

(2) 性質の記述 設計が満たすべき性質（プロパティ）を記述する 記述には一般的に，時間の概念を扱う 時相論理を用いる (2) 性質の記述　　 (property) 設計が満たすべき性質（プロパティ）を記述する 記述には一般的に，時間の概念を扱う 時相論理を用いる (temporal logic) CTL (Computation Tree Logic) LTL (Linear Temporal Logic)

(2) 性質の記述（続き） 【時相論理 (CTL)式の例】 AG(Req → AF Ack) (2) 性質の記述（続き）　　 【時相論理 (CTL)式の例】 AG(Req → AF Ack) 「いつの時点でも，Req が真になると， 　その後，いつか必ず Ack が真になる」 For all paths it is globally (always) true that if Req is true then for all subsequent paths it is true that in future Ack will be true.

(3) 検証 モデル検査器(model checker)と呼ばれる ソフトウェアにより，自動的に検証が行われる (3) 検証　　 モデル検査器(model checker)と呼ばれる ソフトウェアにより，自動的に検証が行われる 性質が成り立つ場合：　検証終了． 性質が成り立たない場合：　 　反例（エラートレース）が出力される． 　それを分析してデバッグする． counterexample (error trace)

モデル検査の実施手順(まとめ) モデル検査器 検査結果 モデル model checker model ＯＫ （状態遷移系） 反例 モデル検査の実施手順(まとめ)　　 モデル検査器 model checker 検査結果 モデル model （状態遷移系） ＯＫ 反例 モデル記述言語 C言語風のもの プロセス代数 性質 property （安全性，活性） The result is either OK or a counterexample 性質の記述 時相論理

他の検証法： Why シミュレーション，テスト 全てのインタラクションや，潜在的なエラーを検査するのはほぼ不可能 定理証明 (simulation, test) 全てのインタラクションや，潜在的なエラーを検査するのはほぼ不可能 定理証明 (theorem proving) 専門的知識・多大な時間を要する．計算可能性の問題．

モデル検査器の例 モデル検査アルゴリズムの原理 状態爆発の軽減の工夫 状態爆発の軽減のその他の工夫 ４．システムとアルゴリズム (systems and algorithms) モデル検査器の例 モデル検査アルゴリズムの原理 状態爆発の軽減の工夫 状態爆発の軽減のその他の工夫

モデル検査器の例(1/2) SMV: カーネギーメロン大学 IEEE Futurebus+ standardのバグ発見 NuSMV: SMVの再実装 SPIN: ベル研究所 ACM Software System Award受賞 UPPAL: スウェーデンとデンマークの大学 実時間システムの検証

モデル検査器の例(2/2) Bogor: カンザス大学 再利用可能なJavaコード LTSA: ロンドン王立大学 プロセス代数に基づくFSP言語，アニメーション Java PathFinder (JPF): NASA Javaのバイトコードの検査

モデル検査アルゴリズムの原理 基本原理： 与えられた性質が成り立つかどうか，すべての計算経路(path)を網羅的に検査する． グラフアルゴリズム 深さ優先探索 (examine all paths) (graph algorithms) (depth-first search)

状態爆発の軽減の工夫 記号モデル検査 (symbolic model checking) - 二分決定木(BDD)による論理式の記号表現と操作． - SMVで実装． 半順序簡約 (partial order reduction) - システムの性質に影響を与えないイベントの生起順序を固定． - SPINで実装． 有界モデル検査 (bounded model checking) - 有限の遷移回数で到達できる状態を論理表現し， 充足可能性判定器(SAT solver)で検証． - NuSMVで実装．

状態爆発の軽減のその他の工夫 モジュール合成(compositional reasoning) 抽象化(abstraction) 対称性(symmetry) 帰納推論(induction)

演習問題 　ここで紹介したモデル検査器のうちの１つについて，それをダウンロードできるサイトを検索して調べ，そのモデル検査器の機能および特徴がどのようなものであるか，サイト内に記載された情報に基づいて報告せよ．