表现系工学特论

表現系工学特論参考文献

ModelChecking,E.M.Clarke,Jr.etal,MITPress(1999)モデル検査（１）

並行システムとモデル検査１．並行システム２．モデル検査３．システムとアルゴリズム１．並行システム並行システムプロセス間通信インタリーブ相互排他デッドロックライブロック，飢餓並行システム(1/7)複数のプロセス(process)が並列(または擬似並列)に動作する計算システム(concurrentsystems)リアクティブ･システム（reactivesystem）

環境からのイベント(event)の入力に実時間(real-time)的に応答する並行システム並行システム(2/7)非同期・交互実行一度に1つのコンポーネントだけが、1ステップ処理を進める同期実行同時に全てのコンポーネントが、1ステップ処理を進める実行方法(asynchronous,interleaved)(synchronous)並行システム(3/7)プロセス間の通信方法共有変数非同期メッセージ通信（キューを用いる）同期メッセージ通信（ハンドシェイク）並行システム(4/7)インタリーブbbbbbbaaaaaaaaプロセスＡbbプロセスＢインターリーブは予期できない制御できない膨大な数の実行経路を生じる(interleave)並行システム(5/7)相互排他共有変数ｍ=5000プロセスＡm=m+1000;プロセスBm=m-1000;MOVA,m(A=5000)MOVB,m(B=5000)ADDA,1000(A=6000)SUBB,1000(B=4000)MOVm,A(m=6000)MOVm,B(m=4000)125346共有変数は相互排他が必要(mutualexclusion)BANK30000030000040000040000040000040000030000030000030000030000040000030万円の口座に10万円仕送りをするBANK30000030000040000040000040000030000020000020000020000030000030000030万円の口座に10万円仕送りをする預入れと引出しが

ほぼ同時の場合並行システム(6/7)デッドロックScanneracquireScanneracquirePrinterCopy12(deadlock)PrinterプロセスＡプロセスＢacquireScanneracquirePrinteracquireScannerCopyacquirePrinteracquireScannerデッドロック並行システム(7/7)ライブロック，飢餓Resourcerequest(livelock)acquireScanneracquirePrinteracquireScanner(starvation)プロセスＢプロセスCプロセスＡacquirerequestacquirerequestプロセスＣは決して資源を獲得できないrequestacquirerequestacquire優先順位の低いプロセス公平性がない(fairness)２．モデル検査モデル検査とは何か有限状態システム検証できる性質モデル検査とは何か

有限状態並行システムの検証を自動で行う技術並行システム

複数のプロセスが並列(または擬似並列)に動作有限状態システム

状態数が有限個の状態遷移系検証

期待される性質(仕様)を満たすことの確認(finitestateconcurrentsystems)(verification)(modelchecking)状態遷移系（オートマトン）状態（ノード）の有限集合初期状態の集合遷移関係（辺の集合）各状態ごとのラベルp,qpq４進カウンタ状態0状態1状態2状態3ticktickticktickresetresetresetreset初期状態イベントラベル（その状態で成り立つ

原始命題）状態数は数百万くらいはＯＫ11pq検証できる性質(1/3)安全性(safety)「悪いことは決して起こらない」という性質＝「良いことは常に成り立つ」活性(liveness)「良いことはいつかは成り立つ」という性質なにが「悪いこと」で，なにが「良いこと」かは，応用目的にあわせて設計者が記述する検証できる性質(2/3)安全性：「悪いことは決して起こらない」決してデッドロックしないこのエレベータは，ドアが開いたまま昇降することは決してないこのメッセージは，暗号化されずに送信されることは決してない検証できる性質(3/3)活性:「良いことはいつか必ず起こる」資源を要求したら，いつか必ず取得できるＯＫボタンを押すと，いつか必ず動作するこのメッセージは必ず宛先に届く３．モデル検査の実施

ソフトウェアのライフサイクル：When&Who

モデル検査の実施手順：How

他の検証法：Whyソフトウェアのライフサイクル：

When&Who

ソフトウェア開発の上流工程で設計者が実施分析設計実装テスト運用ソフトウェアのライフサイクル

（ウォーターフォールモデル）モデリング仕様書設計書コード製品モデル検査の実施手順：How

(1)モデリング(2)性質の記述(3)検証(1)モデリング設計をモデル記述言語で記述し，

モデル（状態遷移系）を定義するC言語風の言語SPIN(Promela言語）SMV,NuSMVプロセス代数に基づく言語LTSA(FSP)モデル記述言語(2)性質の記述

設計が満たすべき性質（プロパティ）を記述する記述には一般的に，時間の概念を扱う

時相論理を用いるCTL(ComputationTreeLogic)LTL(LinearTemporalLogic)(2)性質の記述（続き）

AG(Req→AFAck)「いつの時点でも，Reqが真になると，

その後，いつか必ずAckが真になる」【時相論理(CTL)式の例】(3)検証

モデル検査器(modelchecker)と呼ばれる

ソフトウェアにより，自動的に検証が行われる性質が成り立つ場合：検証終了．性質が成り立たない場合：反例（エラートレース）が出力される．それを分析してデバッグする．モデル検査の実施手順(まとめ)

モデル検査器モデル（状態遷移系）モデル記述言語C言語風のものプロセス代数検査結果ＯＫ反例性質（安全性，活性）性質の記述時相論理他の検証法：Why

シミュレーション，テスト全てのインタラクションや，潜在的なエラーを検査するのはほぼ不可能専門的知識・多大な時間を要する．計算可能性の問題．定理証明４．システムとアルゴリズムモデル検査器の例モデル検査アルゴリズムの原理状態爆発の軽減の工夫状態爆発の軽減のその他の工夫モデル検査器の例(1/2)SMV:カーネギーメロン大学IEEEFuturebus+standardのバグ発見NuSMV:SMVの再実装SPIN:ベル研究所ACMSoftwareSystemAward受賞UPPAL:スウェーデンとデンマークの大学実時間システムの検証モデル検査器の例(2/2)Bogor:カンザス大学再利用可能なJavaコードLTSA:ロンドン王立大学プロセス代数に基づくFSP言語，アニメーションJavaPathFinder(JPF):NASAJavaのバイトコードの検査モデル検査アルゴリズムの原理基本原理：与えられた性質が成り立つかどうか，すべての計算経路(path)を網羅的に検査する．グラフアルゴリズム深さ優先探索状態爆発の軽減の工夫記号モデル検査(symbolicmodelchecking)-二分決定木(BDD)による論理式の記号表現と操作．-SMVで実装．半順序簡約(partialorderreduction)-システムの性質に影響を与えないイベントの生起順序を固定．-SPINで実装．有界モデル検査(boundedmodelchecking)-有限の遷移回数で到達できる状態を論理表現し，

充足可能性判定器(SAT

solver)で検証．-NuSMVで実装．状態爆発の軽減のその他の工夫モジュール合成(compositionalreasoning)抽象化(ab