Systems and Software Verification 10. Fairness Properties システム情報科学府 情報工学専攻 荒木研究室 修士2年 住田 辰雄

目次 10.0 公平性 10.1 時相論理における公平性 10.2 公平性と非決定性 10.3 公平性と公平性仮定 10.4 強公平性と弱公平性 10.5 モデル，それとも性質における公平性？ 2006/10/4 モデル検査勉強会

10.0 公平性 公平性 特定の条件において，イベントは無限に頻繁に発生する（もしくは失敗する） 以下のような表現をすることもある ゲートは無限に頻繁に上昇される (F1) critical sectionへのアクセスが無限に頻繁に発生した場合，アクセスは無限に頻繁に受け付けられる (F2) 以下のような表現をすることもある repeated liveness repeated reachability 2006/10/4 モデル検査勉強会

10.1 時相論理における公平性 公平性 GF P FG 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 モデル検査勉強会

10.1 時相論理における公平性 CTLと公平性 公平性は純粋なCTL論理式を用いて記述することはできない CTL+fairness ただし，AGF Pは可能 AGF P ≡ AG AFP EGF P CTL+fairness 結合子GFとFGが許される 2006/10/4 モデル検査勉強会

10.1 時相論理における公平性 公平性アルゴリズム モデル検査ツール アルゴリズムの適用は容易である CTL+fairnessを使用することより，公平性仮定をモデルの一部として考えることを提案している これは方法論的に見ると， 単純さが（少し）増加する 柔軟性と記述力が（かなり）低下する（10.5節） 2006/10/4 モデル検査勉強会

10.2 公平性と非決定性 公平性は非決定的な連続の形式で記述される 非決定的な選択が発生すると，この選択は公平であると仮定される 例：6面体のサイコロ A(GF1∧ GF2 ∧ GF3 ∧ GF4 ∧ GF5 ∧ GF6) (10.1) 公平性は確率論的性質の抽象化として捕らえることができる 2006/10/4 モデル検査勉強会

10.3 公平性と公平性仮定 Alternating Bit Protocol メッセージ損失する場合がある メッセージを受信すると，送信するか損失する 発信者A メッセージAB 返答BA 受信者B 2006/10/4 モデル検査勉強会

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 モデル検査勉強会

10.4 強公平性と弱公平性 公平性 例 弱公平性 強公平性 Pが絶え間なくリクエストされるならば，Pは無限に頻繁に受け付けられる 2006/10/4 モデル検査勉強会

10.4 強公平性と弱公平性 弱公平性 Pが絶え間なくリクエストされるならば， (FG requests_P => FP) (FG requests_P => GF P) G((FG requests_P) => FP) ≡ G((FG request_P) => GF P) 2006/10/4 モデル検査勉強会

10.4 強公平性と弱公平性 強公平性 Pが絶え間なくリクエストされるならば， (GF requests_P) => FP (GF requests_P) => GF P G((GF requests_P) => FP) ≡ G((GF requests_P) => GF P) 2006/10/4 モデル検査勉強会

10.4 強公平性と弱公平性 強公平性と弱公平性 強公平性ならば弱公平性である 逆は成立しない 弱公平性を保証するスケジューラは強公平性よりも簡単につくることができる 有限システムのモデル検査に対して時相論理を用いるならば，強公平性も弱公平性も違いは存在しない 2006/10/4 モデル検査勉強会

10.5 モデル，それとも性質における公平性？ 公平性の研究は1980年代に多く起こった コンポーネントに対する公平並列操作をもつ並行性のあるモデルに対する研究 このような数学的モデルを建てることは複雑である 技術的問題 どの段階で公平性仮定を適用するか モデルをオートマトンと公平性仮定の組として考えることが一番よい方法である SMVなどが採用している 2006/10/4 モデル検査勉強会