|
平成12年度では、前年度の成果の上に、以下のような成果を得た:
1.有限状態モデルにおいて、以下の提案及び開発を行った。
(1)分散システムを仕様記述可能とした拡張時間オートマトンを開発して、拡張時間オートマトンのAssume-Gurantee形式による自動詳細化検証手法を提案した。ここでの詳細化関係は、Milnerが提案した模倣関係を実時間制約で拡張した時間模倣関係である。
(2)拡張時間オートマトンで仕様記述した分散プロセスが物理的に実装可能であることを保証する条件、いわゆるreceptivenessの自動検証手法を実現した。Receptivenessは、環境と分散プロセスとの無限ゲームで形式化できる。
(3)自動詳細化検証器の実装を行って、計算機実験により、提案手法の有効性を示した。
2.無限状態モデルにおいて、時間ステートチャートのAssume-Gurantee形式による演繹的詳細化検証手法を開発した。さらに、receptivenessの演繹的検証手法を実現した。
現在、以下の検討項目を研究中である:
1.時間ステートチャートのAssume-Gurantee形式による演繹的詳細化検証手法の実装及び実問題への適用。
2.分散システムのより高度なモデル化として、ハイブリッドオートマトンへの拡張。
|
