| 研究概要 |
耐故障分散アルゴリズムであるコンセンサスアルゴリズムに対し,モデル検査という検証法によって,アルゴリズムの正しさを自動的に検証する手法について研究した.コンセンサス問題は,分散システムの耐故障化において基礎となる問題であるが,一般に分散アルゴリズムは設計・検証が困難なため,上記手法の発展は,ディペンダブル分散システム開発の容易化に寄与する.
平成21年度の具体的な研究成果は,以下の二つである.
まず,平成20年度に開発した,モデル検査とインダクションを組み合わせる手法を,検証の専門家ではなく,アルゴリズムの設計者が利用できる仕組みを構築した.この仕組みは,(1) アルゴリズムの記述のための専用言語,および,(2) アルゴリズム記述から数式による動作記述への変換系,からなる,この仕組みを,C言語を用いて実装し,数種類のコンセンサスアルゴリズムを適用例として,実際に検証を行えることを示した.
成果のもう一つは,平成20年度に開発した検証手法の,分散システムの異なる計算モデルへの適用である.これまでに開発した検証手法は,ラウンドモデルとよばれる抽象度の高い分散計算のモデルを前提としていた.そこで,より抽象度の低いモデル上で,現実のプログラムレベルに近い言語(具体的にはPROMELA)で記述されたアルゴリズムへの,開発した検証手法の適応を実現した.ただし,正確性の基準のうち活性の検証については,ラウンドモデルと異なりプロセスがブロッキングし得るので,今後の課題とした.
|
