2008 Fiscal Year Annual Research Report
ディペンダブル分散システム実現のための耐故障アルゴリズムのモデル検査
| Project/Area Number |
20700026
|
|---|
| Research Institution | Osaka University |
|---|
Principal Investigator |
土屋 達弘 Osaka University, 大学院・情報科学研究科, 准教授 (30283740)
|
|---|
| Keywords | 分散アルゴリズム / モデル検査 / 仕様検証 |
|---|
| Research Abstract |
ネットワーク上に構築される情報システムである分散システムを対象に, 検証技術の開発を行った. 具体的には, 代表的な耐故障分散アルゴリズムであるコンセンサスアルゴリズムに対し, モデル検査という検証法を用いて, アルゴリズムの正しさを自動的に検証する手法について研究した. 本年度の研究成果は以下の二つである.
まず, 検証できる対象の規模の向上を実現した. モデル検査を直接適用する検証手法では, システムがコンピュータ3台もしくは4台という小規模な場合についてしか, 検証を行うことができなかった. これを, 8台程度に拡大することに成功した. これは, モデル検査の範囲をアルゴリズムの動作のごく一部に限定し, 動作全体の検証は, モデル検査の結果とインダクションを組み合わせることで検証するというアプローチによって実現した.
これと並行して, 分散アルゴリズムの開発者が, 容易に検証を実行できることを目指し, 関連するツール群を作成した. より具体的には, 擬似コードをそのまま表現できる計算機言語を設計し, 擬似コードで記述された検証対象のアルゴリズムを入力することで, 自動的に正しさを検証することができる手法を開発した. 設計した言語に従って記述されたアルゴリズムは, 作成した変換プログラムによって, モデル検査システムSPINの入力言語PROMELAに自動的に変換される. こうして得られたPROMELAモデルにSPINを適用することで, アルゴリズムの自動検証が実現される.
|
