|
本研究では、高信頼性ネットワークソフトウエアの開発を目指したものである。故障などが生じてシステムが異常な状況になっても、自動的な回復をするプログラム(解法)は、自己安定分散アルゴリズムと呼ばれている。本研究は、自己安定分散アルゴリズムの正しさを検証する手法について研究を行った。今年度は、以下の二点の進展を得た。
1.機械的検証法の研究
自己安定分散アルゴリズムは、どのような種類の故障からも自動回復可能でなければならないが、本当にその性質が満たされているかの検証は困難である。短いアルゴリズムであっても手作業による検証には手間と時間がかかり、また間違いを犯しやすい。
この問題を解決するために、自己安定アルゴリズムの正当性を機械的に検証するシステムを開発した。利用者は、ファイルにまずアルゴリズムを記述し、そしてアルゴリズムが満たすべき仕様(回復すべきシステムの正常な状態)を記述する。そして、検証システムはそのファイルを読込んで、可能なシステムの振る舞い全てをシミュレーションによって調べ、システムの仕様に合致するかを検査する。このシステムは昨年度より引き続いて開発を行っており、今年度は仕様記述の検討を行い、機能拡張を行った。
2.対話的検証システムの開発
昨年度は、自己安定分散アルゴリズムの可視化シミュレータの開発を行ったが、今年度はこれを拡張した。上述した検証システムと統合して対話的に自己安定分散アルゴリズムを検証可能とするシステムを開発し、開発途中の自己安定分散アルゴリズムの誤りを分かりやすく見つけることを可能とした。
|
