2012 Fiscal Year Research-status Report
動的ハイブリッドオートマトンによる動的再構成可能組込みシステムの高度な設計検証
| Project/Area Number |
24500034
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Research Institution | Kanazawa University |
|---|
Principal Investigator |
山根 智 金沢大学, 電子情報学系, 教授 (70263506)
|
|---|
| Project Period (FY) |
2012-04-01 – 2015-03-31
|
| Keywords | ハイブリッドシステム / モデル検査 / 仕様記述 / 組込みシステム / CEGAR |
|---|
| Research Abstract |
本年度は設計検証手法に関する理論を主に開発して仕様記述言語と検証手法を構築し，その手法を用いてシステム仕様記述の事例を開発した．また，設計検証手法の実装にも取り掛かった．
(1)仕様記述言語の開発：仕様記述言語として動的ハイブリッドオートマトンの構文と意味を開発する．この言語の構文は，CPUとDRPとの協調システムを記述するために，ハイブリッドオートマトンをステートチャートやデータ送受信などで拡張するものである．この言語の意味の定義は，操作的意味論を用いて行った．
(2)動的再構成可能組込みシステムの仕様記述：動的ハイブリッドオートマトンを用いて，動的再構成可能組込みシステムをソフトウェア(CPU)とハードウェア(DRP)との協調システムとして仕様記述した．これにより，動的再構成可能組込みシステムが動的ハイブリッドオートマタの並列合成により仕様記述できることを明らかにした．
(3)検証手法の開発：並列動作とハイブリッド性による検証時の状態爆発を抑制するために，動的な構成変化毎に，ハイブリッド性とデータを抽象化精錬する動的ハイブリッドCEGAR(CounterExample Guided Abstraction Refinement)の手法を開発した．さらに，“線形不等式を対象とした一階述語論理の限定記号消去ライブラリ”（周波数変化を記号処理するライブラリ）（小野，山根，電情通学会comp研,2011）を用いて，動的ハイブリッドCEGARの実装に着手した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究の目的は、ソフトウェア(CPU)とハードウェア(DRP)との協調システムの観点から，動的再構成可能組込みシステムの高度な設計検証手法を構築することである．ここで，CPUはCPUスケジューラとタスクからなるリアルタイムシステムである．一方，動的再構成可能プロセッサはDRPスケジューラやコタスク(MPEG,JPEG等の処理)などからなり，並列動作するコタスクの数が動的に変化して，そのコタスクの構成に依存して周波数が動的に変化する動的ハイブリッドオートマタの並列システムである．
研究期間内に，以下のことを明らかにするものである．
（1）コタスクの生成消滅やキュー，CPU-DRP間データ転送，状態の階層並列性（ステートチャート）を表現できる動的ハイブリッドオートマトンの構文と意味を明らかにすることは概ね達成できた．
（2)動的ハイブリッドオートマトタの並列システムにより，動的再構成，つまりソフトウェア(CPU)とハードウェア(DRP)との協調システムがシステム仕様記述できることを明らかにすることも概ね達成できた.
（3）並列動作やハイブリッド性，データなどによる検証時の状態爆発を抑制することが重要である．そこで，CEGAR(CounterExample Guided Abstraction Refinement)とon-the-flyの考えを融合して，システムの動的な構成の変化に応じて，ハイブリッド性やデータを抽象化して，その抽象モデルを精錬して検証する，動的ハイブリッドオートマタに対応した動的ハイブリッドCEGARを開発した。しかし，実用レベルのシステム検証できることを明らかにすることは、現在実装中であり、平成２５年度、２６年度に達成する予定である．このための準備は平成２４年度に実現できたので、概ね達成できたことになる．
|
| Strategy for Future Research Activity |
平成２４年度に開発した理論をもとに、今後は以下の推進方策で研究を進める．前年度の成果を継続して検討するとともに，検証器を実装して，システム仕様記述の事例の実証実験を行う．さらに，動的再構成組込みシステムのターゲットシステムへの設計検証実験も行い，評価する．これにより，実用レベルのシステム設計検証が実現できたことを明らかにする．
（1）まず，前年度に引き続き検証器を開発する．
（2）次に，検証器を用いて，仕様記述の表現能力などの設計手法及び検証コストなどの検証手法の評価を行って，改善する．
（3）次に，金沢大学電子情報系の集積回路研究室で開発中の動的再構成組込みシステムの画像処理システムを題材として，仕様記述と検証の実験を行い，評価する．
（4）最後に，成果をまとめて，組込みシステムや動的再構成可能システムなどの研究会，国際会議で発表及び論文誌に投稿する．
|
| Expenditure Plans for the Next FY Research Funding |
前年度に、検証器実装に必要な計算機は準備できたので、次年度の研究経費は110万円である．その内訳は出張費90万円と消耗品20万円である．
（１）研究成果が出そろうので、学会発表に90万円を使用する．
その内訳は、国内で開催される国際会議やシンポジュウムなどの研究発表に使用する．
（２）消耗品20万円で、書籍やプリタートナーなどを購入する．
|
