広義の信号処理問題への形式検証法の適用

点击翻译按钮获取中文摘要

画像処理は内包するデータ量が膨大であり、並行処理によって処理を高速化することが不可欠である。この観点から本研究では、マルチスレッドのウェーブレットを応用したアルゴリズムにおいて、マルチスレッドの動作が確実である(連携処理によるタイミングのずれや誤動作を生じない)ことを確認することに重点を起き、このためのアルゴリズムの検証方式について広範な研究を行なってきた。具体的には、尖頭S/N比(PSNR)に関して優れた画像圧縮法を新たに提案し、この圧縮法において、スレッド間でデータ交換を行う際に必要なメッセージ列(MSC)について詳しく調べた。また、MSCが正しい(スレッド間のデータ交換に誤りがない)ことを文法構造を導入することにより確認できる方法を考案した。スレッド間通信全体は文書ファイルとして表現し、これをマルチスレッドシステム交信解析システムへの入力とした。解析システムの構築はメッセージ交換におけるデッドロックの検出を考慮しなければならない。そこで、オペレーティングシステムにおけるデッドロック検出に関する知見を利用し、デッドロックはメッセージ交換における送受のタイミングにおいて生じるというところに留意してデッドロック検出手法を設計した。次にデッドロックが生じてしまった場合、この状態をいかに解消するか、システムにおける他の異常状態は存在するか、また、システムが安定に動作する場合に満たすべき条件が失われた場合の振る舞い(画像の列ベクトルについての水平伝送が完了するまでにいかなる垂直伝送も開始されていない)について解析を進めた。本研究の成果は、画像圧縮ソフトウェアのための動作検証に貢献するのみならず、さらに大規模なソフトウェアであるオペレーティングシステムの設計においても示唆を与えるものである。