2014 Fiscal Year Annual Research Report
動的ハイブリッドオートマトンによる動的再構成可能組込みシステムの高度な設計検証
| Project/Area Number |
24500034
|
|---|
| Research Institution | Kanazawa University |
|---|
Principal Investigator |
山根 智 金沢大学, 電子情報学系, 教授 (70263506)
|
|---|
| Project Period (FY) |
2012-04-01 – 2015-03-31
|
| Keywords | 組込みシステム / ハイブリッドオートマトン / モデル検査 / 抽象化精錬 / 仕様記述 / 形式的検証 / 動的再構成 / CEGAR |
|---|
| Outline of Annual Research Achievements |
ソフトウェア(CPU)とハードウェア(DRP)との協調システムの観点から，動的再構成可能組込みシステムの高度な設計検証手法を構築した．
ここで，CPUはCPUスケジューラとタスクからなるリアルタイムシステムである．一方，動的再構成可能プロセッサはDRPスケジューラやコタスク(MPEG,JPEG等の処理)などからなり，並列動作するコタスクの数が動的に変化して，そのコタスクの構成に依存して周波数が動的に変化する動的ハイブリッドオートマタの並列システムである．研究期間内に，以下の成果を得た．
(1)コタスクの生成消滅やキュー，CPU-DRP間データ転送，状態の階層並列性（ステートチャート）を表現できる動的ハイブリッドオートマトンの構文と意味を開発した．
(2)動的ハイブリッドオートマトタの並列システムにより，動的再構成，つまりソフトウェア(CPU)とハードウェア(DRP)との協調システムをシステム仕様記述した．
(3)並列動作やハイブリッド性，データなどによる検証時の状態爆発を抑制するために，CEGAR(CounterExample Guided Abstraction Refinement)とon-the-flyの考えを融合して，システムの動的な構成の変化に応じて，ハイブリッド性やデータを抽象化して，その抽象モデルを精錬して検証する，動的ハイブリッドオートマタに対応した動的ハイブリッドCEGARを開発して，実用レベルのシステム検証できることを明らかにした．
|
