工学类表现系工学特论

《工学类表现系工学特论》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、表現系工学特論参考文献ModelChecking,E.M.Clarke,Jr.etal,MITPress(1999)モデル検査（１）並行システムとモデル検査１．並行システム２．モデル検査３．システムとアルゴリズム１．並行システム並行システムプロセス間通信インタリーブ相互排他デッドロックライブロック，飢餓並行システム(1/7)複数のプロセス(process)が並列(または擬似並列)に動作する計算システム(concurrentsystems)リアクティブ･システム（reactivesystem）環境からのイベント(event)の入力に実時間

2、(real-time)的に応答する並行システム並行システム(2/7)非同期・交互実行一度に1つのコンポーネントだけが、1ステップ処理を進める同期実行同時に全てのコンポーネントが、1ステップ処理を進める実行方法(asynchronous,interleaved)(synchronous)並行システム(3/7)プロセス間の通信方法共有変数非同期メッセージ通信（キューを用いる）同期メッセージ通信（ハンドシェイク）並行システム(4/7)インタリーブbbbbbbaaaaaaaaプロセスＡbbプロセスＢインターリーブは予期できない制御できない膨大な数

3、の実行経路を生じる(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万

4、円の口座に10万円仕送りをするBANK30000030000040000040000040000030000020000020000020000030000030000030万円の口座に10万円仕送りをする預入れと引出しがほぼ同時の場合並行システム(6/7)デッドロックScanneracquireScanneracquirePrinterCopy12(deadlock)Printerプロセス　Ａプロセス　ＢacquireScanneracquirePrinteracquireScannerCopyacquirePrinteracquir

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

6、限状態並行システムの検証を自動で行う技術並行システム複数のプロセスが並列(または擬似並列)に動作有限状態システム状態数が有限個の状態遷移系検証期待される性質(仕様)を満たすことの確認(finitestateconcurrentsystems)(verification)(modelchecking)状態遷移系（オートマトン）状態（ノード）の有限集合初期状態の集合遷移関係（辺の集合）各状態ごとのラベルp,qpq４進カウンタ状態0状態1状態2状態3ticktickticktickresetresetresetreset初期状態イベントラベル（

7、その状態で成り立つ原始命題）状態数は数百万くらいはＯＫ11pq検証できる性質(1/3)安全性(safety)「悪いことは決して起こらない」という性質＝「良いことは常に成り立つ」活性(liveness)「良いことはいつかは成り立つ」という性質なにが「悪いこと」で，なにが「良いこと」かは，応用目的にあわせて設計者が記述する検証できる性質(2/3)安全性：　「悪いことは決して起こらない」決してデッドロックしないこのエレベータは，ドアが開いたまま昇降することは決してないこのメッセージは，暗号化されずに送信されることは決してない検証できる性質(3

8、/3)活性:「良いことはいつか必ず起こる」資源を要求したら，いつか必ず取得できるＯＫボタンを押すと，いつか必ず動作するこのメッセージは必ず宛先に届く３．モデル検査の実施ソフトウェアのライフサイ