|
本研究では、従来個別に研究されていた形式的手法を統合化して、新しい分散システムの設計支援を実現するものである。そのポイントは、開放型システムとして分散システムをとらえて、実時間モデル及びハイブリッドモデルの観点からモデル化して、自動検証及び演縄的検証により設計の正当性を効率的に保証するものである。以上の観点より、我々は、以下の4つのモデルから、設計支援を実現した。
(1)実時間型開放分散システムのAssume-guarantee方式による自動的設計支援:開放型分散システムの仕様記述言語として開放型時間オートマトンを形式化して、Assume-guarantee方式による時間模倣関係の自動検証及びreceptivenessの自動検証を実現した。これにより、実用レベルの分散システムの段階的詳細化設計が可能となった。
(2)実時間型開放分散システムの演繹的設計支援:開放型分散システムの仕様記述言語として時間ステートチャートを形式化して、演繹的な詳細化検証の公理系を開発した。これにより、無限状態を有する分散ソフトウェアの段階的詳細化設計が可能となった。
(3)実時間型開放分散システムのAssume-guarantee方式による演繹的設計支援:開放型分散システムの仕様記述言語としてクロック遷移モジュールを形式化して、Assume-guarantee方式による演繹的な詳細化検証の公理系及びreceptivenessの演繹的検証を開発した。これにより、実用レベルの分散ソフトウェアの段階的詳細化設計が可能となった。
(4)ハイブリッドモデルに基づく開放分散システムの設計支援:開放型分散システムの仕様記述言語としてフェーズ遷移モジュールを形式化して、演繹的な詳細化検証の公理系を開発した。これにより、制御法則を含む分散ソフトウェァの段階的詳細化設計が可能となった。
今後の課題としては、以上の開発した手法を本格的に計算機に実装して、大規模問題への適用及びその評価がある。
|
