2010 Fiscal Year Annual Research Report
| Project/Area Number |
10F00046
|
|---|
| Research Institution | Hiroshima University |
|---|
Principal Investigator |
原田 耕一 広島大学, 大学院・工学研究院, 教授
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
TALUKDER KHasan 広島大学, 大学院・工学研究院, 外国人特別研究員
|
|---|
| Keywords | 形式検証法 / ウェーブレット変換 / SPIN / Sobelフィルタ / 並行的手法 |
|---|
| Research Abstract |
画像工学において近年良く用いられているマルチスレッドのウェーブレットを応用したアルゴリズムにおいては、動作が確実であることを確認するのが重要であるにもかかわらず、一般的にこの検証は大変困難な問題を内包している。つまり、通常のシミュレーションやテストによってはアルゴリズムの正しさを確実に評価することができない。本研究ではこの問題を解決するため、形式検証法の概念に基づいて、マルチスレッドによって実装されたアルゴリズムの正しさを検証することを目的とし、画像の伝送システムにおいて伝送画像を逐次的に送る方式に的を絞り、逐次伝送の過程で用いられる全ての中間的な画像に対し、形式検証法によってアルゴリズムの正しさを検証する方式を検討した。具体的には、まずモデル検査的手法(SMV)と並行的ウェーブレット変換を画像圧縮に応用する方法についての調査を行い、既存の類似の手法を必要に応じて修正することにより、SPINという形式検証法言語によるアルゴリズム記述法を提案した。次にSPINによって表現されたモデルの信頼性に関する定義を行うとともに、モデル検証のための基礎的な研究を遂行してきた。さらに、モデル検証を具体的な画像に適用してその有効性を評価した。具体的な画像として、Sobelフィルタを適用した画像を作成し、これに対してモデル検証法を適用した。更にはSobelフィルタをハードウェアで実装しているチップのアーキテクチャの調査を行ない、提案手法を高速化(ハードウェア化)するための基礎的な知見を得た。
|
