| 研究課題/領域番号 |
14580368
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 金沢大学 |
|---|
研究代表者 |
山根 智 金沢大学, 自然科学研究科, 教授 (70263506)
|
|---|
| 研究期間 (年度) |
2002 – 2004
|
| 研究課題ステータス |
完了 (2004年度)
|
| 配分額 *注記 |
2,200千円 (直接経費: 2,200千円)
2004年度: 600千円 (直接経費: 600千円)
2003年度: 1,000千円 (直接経費: 1,000千円)
2002年度: 600千円 (直接経費: 600千円)
|
|---|
| キーワード | ハイブリッドモデル / 組込みシステム / 高信頼性設計方法 / 演繹的詳細化検証 / モジュール演繹的検証 / モデル検査 / プリエンプティブスケジューラ / 確率ハイブリッドオートマトン / 非線形ハイブリッドシステム / 確率ハイブリッドシステム / 到達可能解析 / 近似解析 / 確率時間オートマトン / 確率時間時相論理 / 演繹的検証 / 詳細化検証 / 仕様記述 / 定理証明 / 確率 / 模倣検証 |
|---|
| 研究概要 |
組込み型システムはアナログ環境に組み込まれたデジタルな実時間システムであり、ハイブリッドシステム(いわゆる、アナログ動作とデジタル動作が混在するシステム)と考えることができて、信頼性が保証できる設計方法論の構築が要望されている分野である。従来の研究では、詳細化検証、モジュール化、既存手法との連携などの点が考慮されていない。本研究では、詳細化検証、既存の開発手法との連携、確率の導入によるモデルの構築などに着目して、定理証明技術や自動検証技術を駆使しながら、信頼性が保証できる設計方法論の構築を行った。
具体的には、本研究では、以下の研究成果をあげた。
(1)ハイブリッドシステムの段階的詳細化開発を可能とするために、詳細化写像を用いた、演繹的な詳細化検証理論を開発して、実験的に有効性を実証した。
(2)ハイブリッドシステムのモジュール毎の仕様記述と検証の手法を可能とするために、フェーズ遷移モジュールとそのモジュール的演繹検証、receptivenessの演繹的検証を実現して、Stepを用いて、実験的に有効性を実証した。
(3)ハイブリッドシステムの重要な事例として、プリエンプティブスケジューラがある。プリエンプティブスケジューラを含む、リアルタイムソフトウェアをハイブリッドシステムとしてモデル化して、仕様記述する手法とそのスケジューラビリティ検証する手法を開発した。事例を用いて、実験的に有効性を実証した。
(4)既存のハイブリッドシステムの開発では、制御理論に基づく制御仕様が使われている。制御仕様からハイブリッドモデルへの変換を含む、統合的な開発手法を開発して、現実的な事例により、実験的に有効性を実証した。
(5)ハイブリッドシステムのランダム性やソフトリアルタイム性を扱うために、確率の概念を導入して、確率線形ハイブリッドオートマトンを開発して、その記号的な検証理論を開発した。
|
