| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2008-04-23 14:00 耐故障分散アルゴリズムに対するPROMELAモデルの生成 ○南川恭洋・土屋達弘・菊野 亨（阪大）  CPSY2008-5 DC2008-5 |
|
| 抄録 | （和） | コンセンサス問題は，耐故障分散システムを実現する上での重要な基本問題である． しかし，コンセンサスアルゴリズムの設計は難しく，フォールトが混入しがちである．そのため，アルゴリズムの検証が不可欠といえる．本研究では，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 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 / / / / | |
| 文献情報 | 信学技報, vol. 108, no. 15, DC2008-5, pp. 25-30, 2008年4月. | |
| 資料番号 | DC2008-5 | |
| 発行日 | 2008-04-16 (CPSY, DC) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | CPSY2008-5 DC2008-5 |
|
| 研究会情報 | |
| 研究会 | DC CPSY |
| 開催期間 | 2008-04-23 - 2008-04-23 |
| 開催地（和） | 東大・武田ホール |
| 開催地（英） | Tokyo Univ. |
| テーマ（和） | ディペンダブルコンピューティングシステムおよび一般 （共催： JST CREST 「アーキテクチャと形式的検証の協調による超ディペンダブルVLSI」） |
| テーマ（英） | Dependable Computing Systems, etc. |
| 講演論文情報の詳細 | |
| 申込み研究会 | DC |
| 会議コード | 2008-04-DC-CPSY |
| 本文の言語 | 日本語 |
| タイトル（和） | 耐故障分散アルゴリズムに対する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 |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 南川 恭洋 / Takahiro Minamikawa / ミナミカワ タカヒロ |
| 第1著者 所属（和/英） | 大阪大学 (略称： 阪大) Osaka University (略称： Osaka Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 土屋 達弘 / Tatsuhiro Tsuchiya / ツチヤ タツヒロ |
| 第2著者 所属（和/英） | 大阪大学 (略称： 阪大) Osaka University (略称： Osaka Univ.) |
| 第3著者 氏名（和/英/ヨミ） | 菊野 亨 / Tohru Kikuno / キクノ トオル |
| 第3著者 所属（和/英） | 大阪大学 (略称： 阪大) Osaka University (略称： Osaka Univ.) |
| 講演者 | 第1著者 |
| 発表日時 | 2008-04-23 14:00:00 |
| 発表時間 | 30分 |
| 申込先研究会 | DC |
| 資料番号 | CPSY2008-5, DC2008-5 |
| 巻番号（vol） | vol.108 |
| 号番号（no） | no.14(CPSY), no.15(DC) |
| ページ範囲 | pp.25-30 |
| ページ数 | 6 |
| 発行日 | 2008-04-16 (CPSY, DC) |
[研究会発表申込システムのトップページに戻る]