研究課題
本年度は前年度に構築したステートチャートの設計検証理論を発展させて、最重要な動的再構成可能組込みシステムをターゲットとして、設計検証手法を開発した。動的再構成可能組込みシステムは構成要素の生成と消滅があり、オブジェクト指向におけるオブジェクトの生成と消滅の概念によりモデル化できることに着目した。動的再構成可能プロセッサの設計検証に関しては以下の技術を開発した。(1) 構成要素の生成と消滅を表現するために、オブジェクト指向のオブジェクトの生成と消滅の概念を含む仕様記述言語を開発した。(2) 動的な構成の変化毎に周波数が変化することを表現するために、ハイブリッドオートマトンの概念を含む仕様記述言語を開発した。(3) 構成要素の内部動作が複雑であるので、ステートチャートの概念を含む仕様記述言語を開発した。(4) 構成要素の動的な生成と消滅を検証するために、生成される最大の構成要素を用意して、生成されるとアクティブにして、消滅するとインアクティブにするように構成要素を記述して、従来の静的なシステムに帰着して検証を実現した。現在、述語抽象化精錬による自動検証手法を検討中である。
すべて 2009 2008
すべて 雑誌論文 (3件) (うち査読あり 3件) 学会発表 (1件)
電子情報通信学会論文誌 J91-D-I, No. 1
ページ: 25-38
コンピュータソフトウェア Vol. 25, No. 3
ページ: 148-193
ページ: 81-87
