2000 Fiscal Year Annual Research Report
自動故障回復を行なうコンピューターネットワークアルゴリズム
| Project/Area Number |
11780229
|
|---|
| Research Institution | Hiroshima University |
|---|
Principal Investigator |
角川 裕次 広島大学, 工学部, 助教授 (80253110)
|
|---|
| Keywords | 自己安定 / 分散システム / 分散アルゴリズム |
|---|
| Research Abstract |
本研究では、高信頼性ネットワークソフトウエアの開発を目指したものである。故障などが生じてシステムが異常な状況になっても、自動的な回復をするプログラム(解法)は、自己安定分散アルゴリズムと呼ばれている。本研究は、自己安定分散アルゴリズムの正しさを検証する手法について研究を行った。今年度は、以下の二点の進展を得た。
1.機械的検証法の研究
自己安定分散アルゴリズムは、どのような種類の故障からも自動回復可能でなければならないが、本当にその性質が満たされているかの検証は困難である。短いアルゴリズムであっても手作業による検証には手間と時間がかかり、また間違いを犯しやすい。
この問題を解決するために、自己安定アルゴリズムの正当性を機械的に検証するシステムを開発した。利用者は、ファイルにまずアルゴリズムを記述し、そしてアルゴリズムが満たすべき仕様(回復すべきシステムの正常な状態)を記述する。そして、検証システムはそのファイルを読込んで、可能なシステムの振る舞い全てをシミュレーションによって調べ、システムの仕様に合致するかを検査する。このシステムは昨年度より引き続いて開発を行っており、今年度は仕様記述の検討を行い、機能拡張を行った。
2.対話的検証システムの開発
昨年度は、自己安定分散アルゴリズムの可視化シミュレータの開発を行ったが、今年度はこれを拡張した。上述した検証システムと統合して対話的に自己安定分散アルゴリズムを検証可能とするシステムを開発し、開発途中の自己安定分散アルゴリズムの誤りを分かりやすく見つけることを可能とした。
|
-
[Publications] 角川: "A Universal Self-Stabilizing Mutual Exclusion Algorithm"京都大学数理解析研究所講究録. (発表予定).
-
[Publications] Mori: "Multilingual system using internet imaging"Electronic Imaging 2001. 4311(論文番号04). (2001)
-
[Publications] 角川: "自己安定分散アルゴリズムの自動検証システム"情報処理学会ソフトウエア工学研究会. SE-128. 9-16 (2000)
-
[Publications] 山下: "自己安定分散アルゴリズムの可視化システムの開発"情報処理学会全国大会. 61(論文番号2Q-04). (2000)
-
[Publications] 川本: "拡張独立点集合問題を解く自己安定分散アルゴリズム"情報処理学会全国大会. 61(論文番号2Q-05). (2000)
-
[Publications] 森: "ビットマップ化による多言語語学教材システム"情報処理学会全国大会. 61(論文番号5S-02). (2000)
-
[Publications] 吉村: "確率的コーラムシステムに基づいた負荷分散アルゴリズムとその実験的評価"情報処理学会全国大会. 61(論文番号6J-07). (2000)
