2014 年度研究成果報告書

動的ハイブリッドオートマトンによる動的再構成可能組込みシステムの高度な設計検証

研究課題

研究課題/領域番号	24500034
研究種目	基盤研究(C)
配分区分	基金
応募区分	一般
研究分野	ソフトウエア
研究機関	金沢大学
研究代表者	山根智金沢大学, 電子情報学系, 教授 (70263506)
研究期間 (年度)	2012-04-01 – 2015-03-31
キーワード	組込みシステム / ハイブリッドオートマトン / モデル検査 / 抽象化精錬 / 仕様記述 / 形式的検証 / 動的再構成可能システム / CEGAR
研究成果の概要	動的再構成可能組込みシステムは，ソフトウェア(汎用CPU)とハードウェア(動的再構成可能プロセッサ(DRP))が協調して，低消費電力で多様な機能を実現する革新的なアーキテクチャであり，複雑な構成と動作を有している．本研究では，①動的ハイブリッドオートマトンの開発，②その抽象化精錬検証の開発により，コタスクの生成消滅，周波数の動的変化，状態の階層並列性などを扱える設計検証を実現して，動的再構成可能組込みシステムの高度な設計検証技術を確立して，その有効性を実証する．
自由記述の分野	形式的手法