工学类表现系工学特论 34页

表現系工学特論参考文献ModelChecking,E.M.Clarke,Jr.etal,MITPress(1999)モデル検査（１）並行システムとモデル検査１．並行システム２．モデル検査３．システムとアルゴリズム\n１．並行システム並行システムプロセス間通信インタリーブ相互排他デッドロックライブロック，飢餓\n並行システム(1/7)複数のプロセス(process)が並列(または擬似並列)に動作する計算システム(concurrentsystems)リアクティブ･システム（reactivesystem）環境からのイベント(event)の入力に実時間(real-time)的に応答する並行システム\n並行システム(2/7)非同期・交互実行一度に1つのコンポーネントだけが、1ステップ処理を進める同期実行同時に全てのコンポーネントが、1ステップ処理を進める実行方法(asynchronous,interleaved)(synchronous)\n並行システム(3/7)プロセス間の通信方法共有変数非同期メッセージ通信（キューを用いる）同期メッセージ通信（ハンドシェイク）\n並行システム(4/7)インタリーブbbbbbbaaaaaaaaプロセスＡbbプロセスＢインターリーブは予期できない制御できない膨大な数の実行経路を生じる(interleave)\n並行システム(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)\nBANK30000030000040000040000040000040000030000030000030000030000040000030万円の口座に10万円仕送りをする\nBANK30000030000040000040000040000030000020000020000020000030000030000030万円の口座に10万円仕送りをする預入れと引出しがほぼ同時の場合\n並行システム(6/7)デッドロックScanneracquireScanneracquirePrinterCopy12(deadlock)Printerプロセス　Ａプロセス　ＢacquireScanneracquirePrinteracquireScannerCopyacquirePrinteracquireScannerデッドロック\n並行システム(7/7)ライブロック，飢餓Resourcerequest(livelock)acquireScanneracquirePrinteracquireScanner(starvation)プロセス　ＢプロセスCプロセス　ＡacquirerequestacquirerequestプロセスＣは決して資源を獲得できないrequestacquirerequestacquire優先順位の低いプロセス公平性がない(fairness)\n２．モデル検査モデル検査とは何か有限状態システム検証できる性質\nモデル検査とは何か有限状態並行システムの検証を自動で行う技術並行システム複数のプロセスが並列(または擬似並列)に動作有限状態システム状態数が有限個の状態遷移系検証期待される性質(仕様)を満たすことの確認(finitestateconcurrentsystems)(verification)(modelchecking)\n状態遷移系（オートマトン）状態（ノード）の有限集合初期状態の集合遷移関係（辺の集合）各状態ごとのラベルp,qpq４進カウンタ状態0状態1状態2状態3ticktickticktickresetresetresetreset初期状態イベントラベル（その状態で成り立つ原始命題）状態数は数百万くらいはＯＫ11pq\n検証できる性質(1/3)安全性(safety)「悪いことは決して起こらない」という性質＝「良いことは常に成り立つ」活性(liveness)「良いことはいつかは成り立つ」という性質なにが「悪いこと」で，なにが「良いこと」かは，応用目的にあわせて設計者が記述する\n検証できる性質(2/3)安全性：　「悪いことは決して起こらない」決してデッドロックしないこのエレベータは，ドアが開いたまま昇降することは決してないこのメッセージは，暗号化されずに送信されることは決してない\n検証できる性質(3/3)活性:「良いことはいつか必ず起こる」資源を要求したら，いつか必ず取得できるＯＫボタンを押すと，いつか必ず動作するこのメッセージは必ず宛先に届く\n３．モデル検査の実施ソフトウェアのライフサイクル：When&Whoモデル検査の実施手順：How他の検証法：Why\nソフトウェアのライフサイクル：When&Whoソフトウェア開発の上流工程で設計者が実施分析設計実装テスト運用ソフトウェアのライフサイクル（ウォーターフォールモデル）モデリング仕様書設計書コード製品\nモデル検査の実施手順：How(1)モデリング(2)性質の記述(3)検証\n(1)モデリング設計をモデル記述言語で記述し，モデル（状態遷移系）を定義するC言語風の言語SPIN(Promela言語）SMV,NuSMVプロセス代数に基づく言語LTSA(FSP)モデル記述言語\n(2)性質の記述設計が満たすべき性質（プロパティ）を記述する記述には一般的に，時間の概念を扱う時相論理を用いるCTL(ComputationTreeLogic)LTL(LinearTemporalLogic)\n(2)性質の記述（続き）AG(Req→AFAck)「いつの時点でも，Reqが真になると，　その後，いつか必ずAckが真になる」【時相論理(CTL)式の例】\n(3)検証モデル検査器(modelchecker)と呼ばれるソフトウェアにより，自動的に検証が行われる性質が成り立つ場合：　検証終了．性質が成り立たない場合：反例（エラートレース）が出力される．それを分析してデバッグする．\nモデル検査の実施手順(まとめ)モデル検査器モデル（状態遷移系）モデル記述言語C言語風のものプロセス代数検査結果ＯＫ反例性質（安全性，活性）性質の記述時相論理\n他の検証法：Whyシミュレーション，テスト全てのインタラクションや，潜在的なエラーを検査するのはほぼ不可能専門的知識・多大な時間を要する．計算可能性の問題．定理証明\n４．システムとアルゴリズムモデル検査器の例モデル検査アルゴリズムの原理状態爆発の軽減の工夫状態爆発の軽減のその他の工夫\nモデル検査器の例(1/2)SMV:カーネギーメロン大学IEEEFuturebus+standardのバグ発見NuSMV:SMVの再実装SPIN:ベル研究所ACMSoftwareSystemAward受賞UPPAL:スウェーデンとデンマークの大学実時間システムの検証\nモデル検査器の例(2/2)Bogor:カンザス大学再利用可能なJavaコードLTSA:ロンドン王立大学プロセス代数に基づくFSP言語，アニメーションJavaPathFinder(JPF):NASAJavaのバイトコードの検査\nモデル検査アルゴリズムの原理基本原理：　与えられた性質が成り立つかどうか，すべての計算経路(path)を網羅的に検査する．グラフアルゴリズム深さ優先探索\n状態爆発の軽減の工夫記号モデル検査(symbolicmodelchecking)-二分決定木(BDD)による論理式の記号表現と操作．-SMVで実装．半順序簡約(partialorderreduction)-システムの性質に影響を与えないイベントの生起順序を固定．-SPINで実装．有界モデル検査(boundedmodelchecking)-有限の遷移回数で到達できる状態を論理表現し，充足可能性判定器(SATsolver)で検証．-NuSMVで実装．\n状態爆発の軽減のその他の工夫モジュール合成(compositionalreasoning)抽象化(abstraction)対称性(symmetry)帰納推論(induction)\n演習問題ここで紹介したモデル検査器のうちの１つについて，それをダウンロードできるサイトを検索して調べ，そのモデル検査器の機能および特徴がどのようなものであるか，サイト内に記載された情報に基づいて報告せよ．\n更多资源xiti123.taobao.com初二语文初二英语初二数学初二物理初二政治初二历史初二地理初二生物