| 研究概要 |
本研究はエ一ジェントの分散制約充足に基づいて,計算機システムにおけるソフトウェアの検証およびハードウェアの診断を行うシステムのモデルを開発し,それを実装し評価することを目的として,3年間の計画で実施している.
本年度はその最終年度として,まず,ソフトウェアの検証のうち特にこれまで検討してきた停止性の検証を引き続き取り上げ,エ一ジェント間の制約を二分決定グラフ(BDD)を用いて効率的に充足する手法とその評価結果をまとめて公表した.さらに,本研究で対象としている書換え系言語において,プログラム自らが自己反映的に自分自身の正当性の検証を行うための実装上のフレームワークとして独創的なメタレベル計算モデルを開発して発表した.
次に,ハードウェアの診断に関しては,組合せ論理回路の各コンポーネントの機能やそれらの接続に関する仕様を制約として等式で記述し,それを完備化と呼ばれる推論規則で充足性を判定する際に,その計算のNP完全性を少しでも緩和するために複数のエ一ジェントがそれぞれ1つの簡約順序を担当して分散して自律的に推論しながらも,独自の真偽維持システムを通して協調することにより,効率的な制約充足判定を実現する手法を開発し発表した.さらに,エ一ジェントを実装するためのソフトウェアアーキテクチャとしてJava言語に基づく分散オブジェクト指向アーキテクチャを示し,実際にシステムを実装し,典型的なテスト問題により評価した結果,期待されていたような良好なパフォ一マンスを確認することができた.
最後に,3年間のプロジェクトを総括し,成果を整理して関連づけるとともに,今後の課題を抽出した.
|
