研究課題
基盤研究(C)
組込み型システムはアナログ環境に組み込まれたデジタルな実時間システムであり、ハイブリッドシステム(いわゆる、アナログ動作とデジタル動作が混在するシステム)と考えることができて、信頼性が保証できる設計方法論の構築が要望されている分野である。従来の研究では、詳細化検証、モジュール化、既存手法との連携などの点が考慮されていない。本研究では、詳細化検証、既存の開発手法との連携、確率の導入によるモデルの構築などに着目して、定理証明技術や自動検証技術を駆使しながら、信頼性が保証できる設計方法論の構築を行った。具体的には、本研究では、以下の研究成果をあげた。(1)ハイブリッドシステムの段階的詳細化開発を可能とするために、詳細化写像を用いた、演繹的な詳細化検証理論を開発して、実験的に有効性を実証した。(2)ハイブリッドシステムのモジュール毎の仕様記述と検証の手法を可能とするために、フェーズ遷移モジュールとそのモジュール的演繹検証、receptivenessの演繹的検証を実現して、Stepを用いて、実験的に有効性を実証した。(3)ハイブリッドシステムの重要な事例として、プリエンプティブスケジューラがある。プリエンプティブスケジューラを含む、リアルタイムソフトウェアをハイブリッドシステムとしてモデル化して、仕様記述する手法とそのスケジューラビリティ検証する手法を開発した。事例を用いて、実験的に有効性を実証した。(4)既存のハイブリッドシステムの開発では、制御理論に基づく制御仕様が使われている。制御仕様からハイブリッドモデルへの変換を含む、統合的な開発手法を開発して、現実的な事例により、実験的に有効性を実証した。(5)ハイブリッドシステムのランダム性やソフトリアルタイム性を扱うために、確率の概念を導入して、確率線形ハイブリッドオートマトンを開発して、その記号的な検証理論を開発した。
すべて 2004 2003 2002 その他
すべて 雑誌論文 (19件)
情報処理学会論文誌 Vol.45, No.5
ページ: 1367-1375
情報処理学会論文誌 Vol.45, No.6
ページ: 1652-1662
Proc.Third International Workshop on Assurance in Distributed Systems and Networks (ADSN 2004) (IEEE Computer Society)
ページ: 622-627
IPSJ Journal vol.45, No.5
IPSJ Journal vol.45, No.6
LNCS 3207
ページ: 183-195
情報処理学会論文誌 Vol.44, No.3
ページ: 867-914
電子情報通信学会 J86-D1
ページ: 232-247
情報処理学会論文誌 Vol.44, No.8
ページ: 2189-2199
Lecture Notes in Computer Science 2896
ページ: 276-290
IPSJ Journal vol.44, No.3
IEICE trans. J86-D1
Proc.IEEE Workshop on Software Technologies for Future Embedded Systems
ページ: 79-82
IPSJ Journal vol.44, No.8
Poc.IEEE 27th COMPSAC
ページ: 527-533
LNCS 2896
Proc.IEEE RTCSA
ページ: 221-228
The 2002 IKE (CSREA Press)
ページ: 455-461
ページ: 469-475