ハイブリッドモデルによる組込みシステムの高信頼性設計方法論の構築と支援環境の開発

2002 Fiscal Year Annual Research Report

• Project/Area Number: 14580368
• Research Institution: Kanazawa University
• Principal Investigator: 山根 智 金沢大学, 工学部, 助教授 (70263506)
• Keywords: ハイブリッドモデル / 組込みシステム / 詳細化検証 / 仕様記述 / 定理証明

Research Abstract

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

Research Products

• [Publications] 山根 智: "Refinement Theory of Embedded systems based on Hybrid models"IKE'02. 10. 455-461 (2002)
• [Publications] 山根 智: "Formal development methodology of hybrid systems"IKE'02. 10. 469-475 (2002)
• [Publications] 山根 智: "ハイブリッドオートマトンによるリアルタイムソフトウェアの仕様記述とスケジューラビリティ検証"電子情報通信学会技報SS. 18. 19-24 (2002)
• [Publications] 山根 智, 山ノ口 崇: "Formal Verification of schedulability"FICT'03. 1. 209-214 (2003)
• [Publications] 山根 智, 館宜伸: "Refinement Verification of Hybrid Automata"FICT'03. 1. 203-208 (2003)
• [Publications] 山根 智: "ハイブリッドシステムのモジュールの仕様記述と検証の手法"情報処理学会論文誌. 44,3. 730-746 (2003)