| 講演名 | 2008-04-23 耐故障分散アルゴリズムに対するPROMELAモデルの生成(ディペンダブルコンピューティングシステム及び一般) 南川 恭洋, 土屋 達弘, 菊野 亨, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | コンセンサス問題は,耐故障分散システムを実現する上での重要な基本問題である.しかし,コンセンサスアルゴリズムの設計は難しく,フォールトが混入しがちである.そのため,アルゴリズムの検証が不可欠といえる.本研究では,Heard-Ofモデルに基づくコンセンサスアルゴリズムの検証支援を目的として,アルゴリズムからモデル検査器SPINの入力モデルへの変換方法,及び,変換を自動化するためのアルゴリズム記述言語の提案を行う.Heard-Ofモデルとは,故障の可能性がある非同期システムの記述に適したモデルである.また,変換方法の有用性を示すため,既知のコンセンサスアルゴリズムに対して適用実験を行う.フォールとが混入したアルゴリズムの検証では,実際にアルゴリズムのフォールトを検出することができた. |
| 抄録(英) | The consensus problem is fundamental in implementing fault-tolerant distributed systems. However, designing a correct consensus algorithm is difficult. Therefore a verification method for consensus algorithms is necessary. The purpose of this study is to facilitate the verification of Heard-Of model-based consensus algorithms with the SPIN model checker. To this end, we propose a transformation method that generates an input model to SPIN from a given consensus algorithm and an algorithm description language. The Heard-Of model is a computation model which allows one to formally treat fault-prone asynchronous systems. We also show the results of verifying several consensus algorithms with the transformation method to show its usefulness. A notable finding of the case studies was that a design fault was successfully detected in an erroneous algorithm. |
| キーワード(和) | 耐故障分散システム / コンセンサス問題 / モデル検査 / Heard-Ofモデル |
| キーワード(英) | fault-tolerant distributed system / consensus problem / model checking / Heard-Of model |
| 資料番号 | CPSY2008-5,DC2008-5 |
| 発行日 |
| 研究会情報 | |
| 研究会 | CPSY |
|---|---|
| 開催期間 | 2008/4/16(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Computer Systems (CPSY) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 耐故障分散アルゴリズムに対するPROMELAモデルの生成(ディペンダブルコンピューティングシステム及び一般) |
| サブタイトル（和） | |
| タイトル（英） | Generating PROMELA Models of Fault-Tolerant Distributed Algorithms |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 耐故障分散システム / fault-tolerant distributed system |
| キーワード(2)（和/英） | コンセンサス問題 / consensus problem |
| キーワード(3)（和/英） | モデル検査 / model checking |
| キーワード(4)（和/英） | Heard-Ofモデル / Heard-Of model |
| 第 1 著者 氏名（和/英） | 南川 恭洋 / Takahiro MINAMIKAWA |
| 第 1 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science and Technology, Osaka University |
| 第 2 著者 氏名（和/英） | 土屋 達弘 / Tatsuhiro TSUCHIYA |
| 第 2 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science and Technology, Osaka University |
| 第 3 著者 氏名（和/英） | 菊野 亨 / Tohru KIKUNO |
| 第 3 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science and Technology, Osaka University |
| 発表年月日 | 2008-04-23 |
| 資料番号 | CPSY2008-5,DC2008-5 |
| 巻番号（vol） | vol.108 |
| 号番号（no） | 14 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |