| 研究分担者 |
手嶋 茂晴 (株)豊田中央研究所, ソフトウェア研究室, 研究員
濱口 毅 名古屋大学, 情報メディア教育センター, 助手 (90273284)
山本 晋一郎 愛知県立大学, 情報科学部, 助教授 (40240098)
結縁 祥治 名古屋大学, 情報メディア教育センター, 助教授 (70230612)
|
|---|
| 研究概要 |
情報機器のみではなく,家電製品や各種知的機械製品において,マイクロプロセッサを中心とした計算機システムによる制御が必須となっている.このような組込みシステムは,実行時に現実の物理現象と干渉をもつリアルタイムシステムであるため,システムの設計・検証は技術的に難しい.また,開発・製造コスト低減のためのメモリ容量制約,CPU能力制約などが厳しいため,システムの設計・検証における技術革新が望まれている.
本研究では組込み用制御システムの中でも,プログラムの応答時間が被制御系の時間的応答と同程度のシステムであるリーンリアルタイムシステム(lean reral-time system)の設計を対象とした設計・検証支援に関して研究を行った.我々はリーンリアルタイムシステムのプログラム構造やその特性を明らかにし,プログラムモデルとして形式化し,それに基づいて『支援システム:組込み工房』を開発した.
組込み工房は,組込み型制御システムプロトタイプ用設計言語とその処理系.および.ソフトウェア文書管理システムから構成される.本システムを自動車制御用ソフトウェアのプログラムプログラムのプロトタイプ工程に適用したところ,製品と同等性能のハードウェアで動作する実行形式のプログラムを得ることができることが確認できた.
一方.検証についてはシステム化の前提として実時間処理を時間オートマトンを使った形式的検証の有効性を調べた.その結果,時間オートマトン記述を作成する上ではデータの扱いや入力アルファベットの時系列集合の定義方法などに課題があることや.プログラム各部の実行遅延によって.システム全体が受ける動作上の影響に関するプロパティが検証対象として有効であることを示した.
|
