| 研究課題/領域番号 |
11680360
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 金沢大学 (2001)
鹿児島大学 (1999-2000) |
|---|
研究代表者 |
山根 智 金沢大学, 工学部, 助教授 (70263506)
|
|---|
| 研究期間 (年度) |
1999 – 2001
|
| 研究課題ステータス |
完了 (2001年度)
|
| 配分額 *注記 |
1,200千円 (直接経費: 1,200千円)
2001年度: 700千円 (直接経費: 700千円)
2000年度: 500千円 (直接経費: 500千円)
|
|---|
| キーワード | 開放型分散システム / 段階的詳細化 / 詳細化検証 / 時間オートマトン / ハイブリッドモデル / Assume-Guarantee / receptiveness / 仕様記述 / 分散システム / 開放型システム / 実時間処理 / 計算機支援 / 時相論理 / 演繹的検証 / リアルタイム性 / receptive |
|---|
| 研究概要 |
本研究では、従来個別に研究されていた形式的手法を統合化して、新しい分散システムの設計支援を実現するものである。そのポイントは、開放型システムとして分散システムをとらえて、実時間モデル及びハイブリッドモデルの観点からモデル化して、自動検証及び演縄的検証により設計の正当性を効率的に保証するものである。以上の観点より、我々は、以下の4つのモデルから、設計支援を実現した。
(1)実時間型開放分散システムのAssume-guarantee方式による自動的設計支援:開放型分散システムの仕様記述言語として開放型時間オートマトンを形式化して、Assume-guarantee方式による時間模倣関係の自動検証及びreceptivenessの自動検証を実現した。これにより、実用レベルの分散システムの段階的詳細化設計が可能となった。
(2)実時間型開放分散システムの演繹的設計支援:開放型分散システムの仕様記述言語として時間ステートチャートを形式化して、演繹的な詳細化検証の公理系を開発した。これにより、無限状態を有する分散ソフトウェアの段階的詳細化設計が可能となった。
(3)実時間型開放分散システムのAssume-guarantee方式による演繹的設計支援:開放型分散システムの仕様記述言語としてクロック遷移モジュールを形式化して、Assume-guarantee方式による演繹的な詳細化検証の公理系及びreceptivenessの演繹的検証を開発した。これにより、実用レベルの分散ソフトウェアの段階的詳細化設計が可能となった。
(4)ハイブリッドモデルに基づく開放分散システムの設計支援:開放型分散システムの仕様記述言語としてフェーズ遷移モジュールを形式化して、演繹的な詳細化検証の公理系を開発した。これにより、制御法則を含む分散ソフトウェァの段階的詳細化設計が可能となった。
今後の課題としては、以上の開発した手法を本格的に計算機に実装して、大規模問題への適用及びその評価がある。
|
