調停者の選出方法を考慮した分散合意アルゴリズムのPROMELAモデルと検証

• Item type: SIG Technical Reports(1)
• 公開日: 2013-07-10
• タイトル: 調停者の選出方法を考慮した分散合意アルゴリズムのPROMELAモデルと検証
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: モデル
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 信州大学大学院理工学系研究科情報工学専攻
• 著者所属: 信州大学工学部情報工学科
• 著者名: 後藤亮馬; 和崎克己
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 合意問題は分散システムの研究分野において重要な問題の一つであり，非同期分散アルゴリズムにおいては，合意問題が解決されているかを確認することが困難である．本研究では，非同期分散アルゴリズムの正当性を，モデル検査によって検証することを目的として，モデル検査器 SPIN を用いて，非同期分散合意アルゴリズムである Chandra-Toueg アルゴリズムの正当性を検証する．SPIN とは通信プロトコルの検証を目的として提案されたモデル検査ツールであり，使用記述言語 PROMELA で記述された振る舞いを，網羅探査により検査することができる．モデルの作成を行う際には，PROMELA 本来の記述方法では困難であった表現を行うために，グローバルタイムアウト機構などのいくつかの工夫を行った．Chandra-Toueg アルゴリズムで使用されている巡回調停者方式では，調停者が健全か否かを考慮しない．また，実際には調停者変更を行った後，ノード間でのリセット動作などの同期を取るべきである．以上二つの理由から，調停者変更時に健全性の判定機能を追加し，調停者変更後に同期をとる選出方法に変更した．作成した通常モデルと拡張モデルを使用してデットロック検査を行い，正当性を検証した．
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10112981
• 書誌情報: 研究報告ソフトウェア工学（SE）; 巻 2013-SE-181, 号 8, p. 1-7, 発行日 2013-07-10
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会