2010 Fiscal Year Annual Research Report
ディペンダブル分散システム実現のための耐故障アルゴリズムのモデル検査
| Project/Area Number |
20700026
|
|---|
| Research Institution | Osaka University |
|---|
Principal Investigator |
土屋 達弘 大阪大学, 大学院・情報科学研究科, 准教授 (30283740)
|
|---|
| Keywords | 分散アルゴリズム / モデル検査 / 仕様検証 |
|---|
| Research Abstract |
コンセンサスは分散システムの耐故障化における基礎問題であるが,アルゴリズムの設計・検証は一般に困難である.そこで,本研究では,高信頼システムの開発容易化への寄与を目的として,コンセンサスアルゴリズムに対し,自動検証手法であるモデル検査法を適用することで,その設計の正しさを検証する手法について研究した.
平成22年度の具体的な研究成果は,以下の二つである.まず,平成20年度および21年度に開発したモデル検査とインダクションを組み合わせる手法を,4種類のアルゴリズムに対して適用し,包括的な実験的結果を得ることができた.具体的には,アルゴリズムによって異なるが,7プロセス(コンピュータ)から13プロセスの規模のシステム上での動作に関して,アルゴリズムの正しさを検証することができた.また,活性という性質の検証に限定すれば,どのアルゴリズムについても14プロセスの規模の検証が可能であった.
もう一方の成果は,平成21年度に開発した,抽象度の低いモデルにおけるアルゴリズムの検証手法の拡張である.現実のプログラムレベルに近い言語レベルでアルゴリズムを記述した場合,動作が詳細になるために検証できるシステム規模は大幅に制限されるが,より詳細な不具合検出が可能となる.平成21年度の段階では,安全性と活性という二つの正確性の基準について,前者のみ検証が可能であった.本年度は,故障検出に関する能力をモデル化することによって,活性についても検証可能とすることができた.
|
