関連研究 FeaVer について

FeaVer (GUI)

Modex( )

Spin( )

C

Test harness C

Promela

Pan.c

Pan.exe FeaVer

図 4.6: FeaVerの構成

4.5.2 FeaVer とバイナリモデル検査の違い

FeaVerは並行性をもつCプログラムの検査をターゲットにしている。なぜならModex

は、Cの関数をPromelaのプロセスに対応付けし、デッドロックや競合状態を追跡でき るようなモデルを生成することに秀でているからである。それに、対してバイナリモデル 検査では、シーケンシャルに動作するプログラムを保証しようとしている。入力変数の集 合を与えることで呼び出されるC関数列がどのように動作するかを調べるからである。ま た、動作環境を積極的にそのまま利用する点もバイナリモデル検査の特徴でありFeaVer とは異なっている。

4.5.3 FeaVer の利点と不利な点

Test harnessさえ適切に記述できれば、あとはCプログラムを全自動で検査できること

がやはりFeaVerの大きな利点である。配列の境界条件チェックやNULLポインタチェック

を行うc codeをデフォルトで追加してくれることも良い機能である。しかも、GUIで操

作できるのでSpinのオプションの設定などは非常に分かり易い。しかし、FeaVerを使っ ての初めのであるTest harness作成についての理解が難しい。この行程を適切に行うため には、Spinの機能の正確な理解が求められるであろう。つまり、FeaVerはSpinに関して 知識豊かな人のためのツールであり、モデル検査に関して初心者が人に使いこなす事は難 しいと考えられる。これが不利な点である。さらに、FeaVerのマニュアルおいて動的に 確保したメモリ領域の扱い方については全く触れられていない。今後、バイナリモデル検 査において、動的に確保したメモリ領域の監視や局所変数の監視が可能となればFeaVer に対する大きなアドバンテージになると考えている。

第 5 ^{章 おわりに}

5.1 ^まとめ

本研究では、バイナリモデル検査という独自手法を提案し、様々な問題の解決と整理を 行った。まず、バイナリモデル検査手法の概要を整理し、どのような検査手法であるのか を明確化させた。そして、本検査手法を行うことによって得られる利点について考察し た。バイナリモデル検査を行うにあたり、検査対象Cプログラムを検査可能な形に変更す るために内容変更が必要な場合があるので、その変更必要箇所と変更手順を手法として提 案した。次に、このように整理・一般化した検査手法を検査実験としてsortプログラムや lsプログラムなど実際のプログラムに適用し、その効果について考察した。結果として、

ある程度の規模のCプログラムであっても、多少の関数の仕様変更は迫られるものの、プ ログラムフローに関しては、ほとんど変更せずにSpinから直接呼び出して検査可能であ ることが分かった。以上が検査法確立に関しての成果である。またそれに関連して、技術 面に関しての成果もいくつかあった。監視するC変数指定方法とその扱い方に対する考 察や、効率的にメモリ空間を監視するための工夫、Cプログラム中で使用される動的メモ リ空間の取り扱い方に対する問題提起と解決策の提案などが代表的な技術的成果である。

これらの研究成果からバイナリモデル検査を利用すれば、検査コストが少なく、実環境 により近い状態でのCプログラム検査が可能であることが示せた。