Systems and Software Verification 10. Fairness Properties システム情報科学府 情報工学専攻 荒木研究室 修士2年 住田 辰雄 目次 • • • • • • 10.0 公平性 10.1 時相論理における公平性 10.2 公平性と非決定性 10.3 公平性と公平性仮定 10.4 強公平性と弱公平性 10.5 モデル，それとも性質における公平性？ 2006/10/4 モデル検査勉強会 2 10.0 公平性 • 公平性 – 特定の条件において，イベントは無限に頻繁に発生 する（もしくは失敗する） • ゲートは無限に頻繁に上昇される (F1) • critical sectionへのアクセスが無限に頻繁に発生した場合， アクセスは無限に頻繁に受け付けられる (F2) – 以下のような表現をすることもある • repeated liveness • repeated reachability 2006/10/4 モデル検査勉強会 3 10.1 時相論理における公平性 • 公平性 – GF P • AGF gate_raised (F1) • A(GF crit_req => GF crit_in) (F2) – FG P • A(GF crit_in ∨ FG ￢crit_req) (F2) – FGはGFの対偶 2006/10/4 モデル検査勉強会 4 10.1 時相論理における公平性 • CTLと公平性 – 公平性は純粋なCTL論理式を用いて記述す ることはできない • ただし，AGF Pは可能 – AGF P ≡ AG AFP – EGF P – CTL+fairness • 結合子GFとFGが許される 2006/10/4 モデル検査勉強会 5 10.1 時相論理における公平性 • 公平性アルゴリズム – アルゴリズムの適用は容易である • O(| A | | |2 )時間 • モデル検査ツール – CTL+fairnessを使用することより，公平性仮定をモデ ルの一部として考えることを提案している • これは方法論的に見ると， – 単純さが（少し）増加する – 柔軟性と記述力が（かなり）低下する（10.5節） 2006/10/4 モデル検査勉強会 6 10.2 公平性と非決定性 • 公平性は非決定的な連続の形式で記述さ れる – 非決定的な選択が発生すると，この選択は公 平であると仮定される • 例：6面体のサイコロ – A(GF1∧ GF2 ∧ GF3 ∧ GF4 ∧ GF5 ∧ GF6) (10.1) – 公平性は確率論的性質の抽象化として捕らえ ることができる 2006/10/4 モデル検査勉強会 7 10.3 公平性と公平性仮定 • Alternating Bit Protocol – メッセージ損失する場合がある • メッセージを受信すると，送信するか損失する メッセージAB 発信者A 受信者B 返答BA 2006/10/4 モデル検査勉強会 8 10.3 公平性と公平性仮定 • 全ての送信したメッセージは結局は受信される（活性） – 検証すると，失敗する • このモデルは全てのメッセージを損失する可能性がある • メッセージ損失するか，もしくは送信する（活性仮定） – ある送信されたメッセージはこれまで受信されたメッセージの中に存在 する • A(GF ￢loss => G(emitted => F received)) (CTL) • GF￢loss => G(emitted => F received) (PLTL) – 無限に多くのメッセージが発信されたならば，無限に多くのメッセージが 送信される • A(GF ￢loss => (GF emitted => GF received)) • A(ψ1 => (ψ2 => φ) – ψ1 : 公平性仮定 – ψ2 : 繰り返し活性仮定 – φ : 繰り返し活性 2006/10/4 モデル検査勉強会 9 10.4 強公平性と弱公平性 • 公平性 – 弱公平性 – 強公平性 • 例 – Pが絶え間なくリクエストされるならば，Pは無 限に頻繁に受け付けられる 2006/10/4 モデル検査勉強会 10 10.4 強公平性と弱公平性 • 弱公平性 – Pが絶え間なくリクエストされるならば， • Pは割り込みなしにリクエストされるならば – (FG requests_P => FP) – (FG requests_P => GF P) • G((FG requests_P) => FP) ≡ G((FG request_P) => GF P) 2006/10/4 モデル検査勉強会 11 10.4 強公平性と弱公平性 • 強公平性 – Pが絶え間なくリクエストされるならば， • Pが割り込みがあるかもしれないが，繰り返し無限 にリクエストされるならば， – (GF requests_P) => FP – (GF requests_P) => GF P • G((GF requests_P) => FP) ≡ G((GF requests_P) => GF P) 2006/10/4 モデル検査勉強会 12 10.4 強公平性と弱公平性 • 強公平性と弱公平性 – 強公平性ならば弱公平性である • 逆は成立しない – 弱公平性を保証するスケジューラは強公平性 よりも簡単につくることができる – 有限システムのモデル検査に対して時相論理 を用いるならば，強公平性も弱公平性も違い は存在しない 2006/10/4 モデル検査勉強会 13 10.5 モデル，それとも性質における 公平性？ • 公平性の研究は1980年代に多く起こった – コンポーネントに対する公平並列操作をもつ 並行性のあるモデルに対する研究 – このような数学的モデルを建てることは複雑で ある • 技術的問題 • どの段階で公平性仮定を適用するか – モデルをオートマトンと公平性仮定の組として考えること が一番よい方法である – SMVなどが採用している 2006/10/4 モデル検査勉強会 14
© Copyright 2024 ExpyDoc
