2008 Fiscal Year Annual Research Report
述語抽象化検証による大規模組込みシステム向きオブジェクト指向設計自動検証手法
| Project/Area Number |
19500025
|
|---|
| Research Institution | Kanazawa University |
|---|
Principal Investigator |
山根 智 Kanazawa University, 電子情報学系, 教授 (70263506)
|
|---|
| Keywords | オブジェクト指向 / 動的再構成組込みシステム / ハイブリッドオートマトン / 仕様記述言語 / 検証 |
|---|
| Research Abstract |
本年度は前年度に構築したステートチャートの設計検証理論を発展させて、最重要な動的再構成可能組込みシステムをターゲットとして、設計検証手法を開発した。動的再構成可能組込みシステムは構成要素の生成と消滅があり、オブジェクト指向におけるオブジェクトの生成と消滅の概念によりモデル化できることに着目した。動的再構成可能プロセッサの設計検証に関しては以下の技術を開発した。
(1) 構成要素の生成と消滅を表現するために、オブジェクト指向のオブジェクトの生成と消滅の概念を含む仕様記述言語を開発した。
(2) 動的な構成の変化毎に周波数が変化することを表現するために、ハイブリッドオートマトンの概念を含む仕様記述言語を開発した。
(3) 構成要素の内部動作が複雑であるので、ステートチャートの概念を含む仕様記述言語を開発した。
(4) 構成要素の動的な生成と消滅を検証するために、生成される最大の構成要素を用意して、生成されるとアクティブにして、消滅するとインアクティブにするように構成要素を記述して、従来の静的なシステムに帰着して検証を実現した。
現在、述語抽象化精錬による自動検証手法を検討中である。
|
