工学类表系工学特论.ppt

更多资源 状態爆発の軽減の工夫 記号モデル検査 (symbolic model checking) - 二分決定木(BDD)による論理式の記号表現と操作． - SMVで実装． 半順序簡約 (partial order reduction) - システムの性質に影響を与えないイベントの生起順序を固定． - SPINで実装． 有界モデル検査 (bounded model checking) - 有限の遷移回数で到達できる状態を論理表現し，充足可能性判定器(SAT solver)で検証． - NuSMVで実装． 状態爆発の軽減のその他の工夫 モジュール合成(compositional reasoning) 抽象化(abstraction) 対称性(symmetry) 帰納推論(induction) 演習問題 　ここで紹介したモデル検査器のうちの１つについて，それをダウンロードできるサイトを検索して調べ，そのモデル検査器の機能および特徴がどのようなものであるか，サイト内に記載された情報に基づいて報告せよ． 初二语文? 初二英语? 初二数学? 初二物理? 初二政治? 初二历史 ?初二地理? 初二生物 表現系工学特論 参考文献Model Checking, E.M. Clarke, Jr. et al, MIT Press (1999) モデル検査（１）並行システムとモデル検査 １．並行システム ２．モデル検査 ３．システムとアルゴリズム １．並行システム 並行システム プロセス間通信 インタリーブ 相互排他 デッドロック ライブロック，飢餓 並行システム(1/7) 複数のプロセス(process)が並列(または擬似並列)に動作する計算システム (concurrent systems) リアクティブ?システム（reactive system） 環境からのイベント(event)の入力に実時間(real-time)的に応答する並行システム 並行システム(2/7) 非同期?交互実行 一度に1つのコンポーネントだけが、1ステップ処理を進める 同期実行 同時に全てのコンポーネントが、1ステップ処理を進める 実行方法 (asynchronous, interleaved) (synchronous) 並行システム(3/7) プロセス間の通信方法 共有変数 非同期メッセージ通信（キューを用いる） 同期メッセージ通信（ハンドシェイク） 並行システム(4/7) インタリーブ b b b b b b a a a a a a a a プロセスＡ b b プロセスＢ インターリーブは 予期できない 制御できない 膨大な数の実行経路を生じる (interleave) 並行システム(5/7) 相互排他 共有変数 ｍ=5000 プロセスＡ m = m + 1000; プロセスB m = m - 1000; MOV A,m (A=5000) MOV B,m (B=5000) ADD A,1000 (A=6000) SUB B,1000 (B=4000) MOV m,A (m=6000) MOV m,B (m=4000) 1 2 5 3 4 6 共有変数は相互排他が必要 (mutual exclusion) BANK 300000 300000 400000 400000 400000 400000 300000 300000 300000 300000 400000 30万円の口座に10万円仕送りをする BANK 300000 300000 400000 400000 400000 300000 200000 200000 200000 300000 300000 30万円の口座に10万円仕送りをする 預入れと引出しがほぼ同時の場合 並行システム(6/7) デッドロック Scanner acquire Scanner acquire Printer Copy 1 2 (deadlock) Printer プロセス　Ａ プロセス　Ｂ acquire Scanner acquire Printer acquire Scanner Copy acquire Printer acquire Scanner デッドロック 並行システム(7/7) ライブロック，飢餓 Resource request (livelock) acquire Scanner acquire Printer acquire Scanner (starvation) プロセス　Ｂ プロセス　C プロセス　Ａ acquire request acquire request プロセスＣは決して資源を獲得できな