|
今年度は、以下の三点の進展を得た。
1.自動変換手法の研究
ここ数年に渡る研究の成果として、自己安定分散アルゴリズムを抽象的で高水準な形での記述をし、その記述を実際のシステム上で動作するプログラムに「自動変換」する手法を開発した。今年度は、自動変換手法を継続して研究を行った。カンサス州立大学の水野助教授と共同で、いま論文の出版の準備を進めている段階である。
2.機械的検証法の研究
アルゴリズムの記述に高水準な記法を用いることにより、自己安定アルゴリズムの設計はずいぶんと容易になった。それに伴い、アルゴリズムの正しさの理論的な証明を行うのも容易にはなったものの、手間と時間のかかる作業である。この問題を解決するために、自己安定アルゴリズムの正当性を機械的に検証するシステムを開発した。利用者は、ファイルにまずアルゴリズムを記述し、そしてアルゴリズムが満たすべき仕様(回復すべきシステムの正常な状態)を記述する。そして、検証システムはそのファイルを読込んで、可能なシステムの振る舞い全てをシミュレーションによって調べ、システムの仕様に合致するかを検査する。このシステムはまだ実験段階であり、来年度も引き続いて研究を行う予定である。
3.自己安定アルゴリズムの可視化シミュレータの開発
自己安定アルゴリズムは、システムの初期状態や実行のタイミングに関わらず、その正しさが保証されないといけないため、その振る舞いが非常に複雑である。本研究では、自己安定アルゴリズムの直感的理解および、誤りのある自己安定アルゴリズムの問題点を発見するために、自己安定アルゴリズムのシミュレーションに基づいた可視化システムを作成し、その動作を視覚的な観察を可能とした。
|
