| 講演名 | 1999/11/12 記号モデル検査を用いた自己安定アルゴリズムの検証法の提案 土屋 達弘, 長野 伸一, パイディ ロハユ, 菊野 亨, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 自己安定アルゴリズムとは,任意の初期状態から有限時間内で正常状態に遷移する分散アルゴリズムである.本論文では,このような自己安定アルゴリズムに対する自動検証について議論する.アルゴリズムの自己安定性を示すためには,定義上,全ての状態を初期状態として考慮する必要がある.従って,アルゴリズムの挙動を有限状態機械で表現する通常のモデル検査手法では,状態数が指数的に増大してしまい適用が不可能であった.本研究では,この問題を解決するため,記号モデル検査を用いて検証を行うことを提案する.記号モデル検査は,二分決定グラフ(BDD)を用いて状態空間を表現する検証法であり,このBDDは初期状態に依存しないという特色を持つ.具体的には,良く知られた記号モデル検査ツールであるSMVを用いた検証の枠組みを提案する.更に,実際に提案手法を用いてアルゴリズムの間違いを発見した例についても報告する. |
| 抄録(英) | A distributed system is said to be self-stabilizing if it converges to safe states regardless of its initial state. In this paper we present our results of using symbolic model checking to verify distributed algorithms against the self-stabilization property. So far applying model checking to self-stabilizing algorithms has not been successful since there has been no feasible way to examine all possible initial states. To cope with the difficulty, we propose to use symbolic model checking for this purpose. Symbolic model checking is a verification approach which uses boolean functions to compactly represent state spaces and transition relations. Unlike other model checking techniques, symbolic model checking allows multiple initial states and a large part of the computation it needs does not depend on the initial states. We provide a framework in which SMV, a well-known symbolic model checker, can be used for verifying the correctness of algorithms. Then we verify several algorithms by the proposed approach and show its usefulness in detecting errors. |
| キーワード(和) | 自己安定 / 自動検証 / 記号モデル検査 / 分散アルゴリズム |
| キーワード(英) | Self-stabilization / automatic verification / symbolic model checking / distributed algorithms |
| 資料番号 | SS99-49 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 1999/11/12(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | ENG |
| タイトル（和） | 記号モデル検査を用いた自己安定アルゴリズムの検証法の提案 |
| サブタイトル（和） | |
| タイトル（英） | On Symbolic Model Checking Self-Stabilizing Algorithms |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 自己安定 / Self-stabilization |
| キーワード(2)（和/英） | 自動検証 / automatic verification |
| キーワード(3)（和/英） | 記号モデル検査 / symbolic model checking |
| キーワード(4)（和/英） | 分散アルゴリズム / distributed algorithms |
| 第 1 著者 氏名（和/英） | 土屋 達弘 / Tatsuhiro Tsuchiya |
| 第 1 著者 所属（和/英） | 大阪大学大学院基礎工学研究科情報数理系専攻 Department of Informatics and Mathematical Science Graduate School of Engineering Science, Osaka University |
| 第 2 著者 氏名（和/英） | 長野 伸一 / Shin'ichi Nagano |
| 第 2 著者 所属（和/英） | (株)東芝 Toshiba Corporation |
| 第 3 著者 氏名（和/英） | パイディ ロハユ / Rohayu Bt Paidi |
| 第 3 著者 所属（和/英） | (株)マレーシア松下電器 Malaysia Matsushita Electric Corporation |
| 第 4 著者 氏名（和/英） | 菊野 亨 / Tohru Kikuno |
| 第 4 著者 所属（和/英） | 大阪大学大学院基礎工学研究科情報数理系専攻 Department of Informatics and Mathematical Science Graduate School of Engineering Science, Osaka University |
| 発表年月日 | 1999/11/12 |
| 資料番号 | SS99-49 |
| 巻番号（vol） | vol.99 |
| 号番号（no） | 424 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |