|
まず、本年度は基本検討及び情報収集を行った。具体的には、以下の2つの主要な技術を開発した。
(1)モジュール単位の仕様記述を可能とするために、フェーズ遷移モジュールを開発した。フェーズ遷移モジュールは環境との相互作用が記述できる、無限な状態数を表現できる仕様記述言語であり、組込み型システムの一般的な計算モデルである。
(2)モジュール単位の詳細化検証を実現するために、モジュールの実装可能性(いわゆる、receptiveness)の検証手法及びモジュール単位の詳細化検証手法(いわゆる、Assume-guarantee style)を開発した。Receptivenessは実時間性を含めたモデル化では考慮すべき重要な性質であり、ハイブリッドシステムでは、本研究が世界で最初に形式化を提案した。
(3)リアルタイムオペレーティングシステム及び制御システムを対象として、仕様記述及び詳細化検証の実験を行い、評価・改善を行った。
また、国際会議及び研究会で、その成果を発表した。
|
