シンボリック実行を利用したソフトウェアの互換性確認にかんする考察と実験

標準

実験

2つの実験を実施しました。

実験その1は、3つのタイプの仕様変更:追加、修正、削除があった場合のサンプルプログラムにテストプロセスを適用し、すべてのタイプが検出できるかを確認します。

実験その2は、実験その1に加えて、プログラムに3つのタイプのバグが埋め込まれたとき、テストプロセスを適用し、すべてのタイプのバグが検出できるかを確認します。

実験その1

サンプルプログラムは、とある公共施設の入場料の割引率を計算し、返却する機能をもちます。条件によって様々な割引があります。以下がプログラムの仕様です。

If age of a customer is less than or equal to 3, Free (0% of the normal fee)
If Wednesday, 90% of the normal fee
If age of a customer is greater than or equal to 60, 60% of the normal fee
If sex of a customer is female and her age is greater than or equal to 50, 65% of the normal fee
If the memorial day, 80% of the normal fee
If a customer is local citizen, 50% of the normal fee
If after 3 P.M., 70% of the normal fee
If age of a customer is less than or equal to 12, 40% of the normal fee
Note that greater discount rate is applied when multiple conditions are met

※ この仕様はデバッグ工学研究所 松尾谷氏の資料から持ってきました

この仕様に対して、3種類の変更を加えます。

If age of a customer is less than or equal to 3, Free (0% of the normal fee)
If Wednesday, 90% of the normal fee
If age of a customer is greater than or equal to 60, 60% of the normal fee
If sex of a customer is female and her age is greater than or equal to 55 (修正), 65% of the normal fee
If the memorial day, 80% of the normal fee(削除)
If a customer is local citizen, 50% of the normal fee
If after 3 P.M., 70% of the normal fee
If age of a customer is less than or equal to 12, 40% of the normal fee
If January or February, 67% of the normal fee(追加)
Note that greater discount rate is applied when multiple conditions are met

 

変更前後の仕様を実装したソースコードのフローチャートは下図のようになりました。

仕様変更プログラムフロー

わかりづらいかもしれませんが、変更後の仕様のほうのフローチャートで、太字で囲んだ場所が、変更前との差分が生じた場所です。

このプログラムに対して、シンボリック実行を適用します。今回は、Java言語に対応したツールである、SPF (Symbolic Path Finder) を使いました。SPFはNASAが開発したツールで、プログラムを解析するJPF(Java Path Finder)というツールのアドオンとして動作するものです。

インストールはそれほど難しくありません(他のツールに比べれば)。インストール手順は別のエントリーにまとめましたので、参照してみてください:http://blog.utkeiji.com/?p=4

仕様変更前のプログラム(左側のフローチャート)に対して適用した結果、13のテストケースが生成されました。結果を下記の表にまとめます。

仕様変更前プログラムへの適用結果

ここで、一番右の列は、生成されたテストケースを仕様変後のプログラムに流した出力結果です。両者の出力を比較すると、3箇所の差分がありました。青い四角で囲んだ差分は、仕様を「修正」した箇所でした。また、赤い四角で囲んだ差分は、仕様を「削除」した箇所でした。

次に仕様変更後のプログラムに対してツールを適用した結果を、下記の表に示します。15のテストケースが生成されました。

仕様変更後プログラムへの適用結果

 

同様に、テストケースを仕様変更前のプログラムに流した出力結果が一番右の列です。出力同士を比較すると、4箇所の差分がありました。緑の四角で囲んだ部分です。これらはすべて仕様を「追加」した箇所でした。

この結果から、シンボリック実行を利用したテストプロセスによって、3種類すべての仕様変更が検出できることがわかりました。
実験その2

次の実験では、実験その1のプログラムに対して、3種類のバグを埋め込んだ場合を考えます。変更前と、バグを埋め込んだプログラムそれぞれのフローチャートを下記に示します。

バグ埋め込みプログラムフロー

点線で囲まれた箇所が、バグを埋め込んだところです。

このプログラムに対してシンボリック実行を実施します。そして、実験その1と同様に2つのプログラムの出力を比較した結果を下記に示します。

バグなしプログラムへの適用結果

赤い四角で囲まれた箇所は、誤って「削除」したバグの部分、青い四角は、誤って「修正」したバグの部分を検出することができました。

次にバグを埋め込んだプログラムを対象にシンボリック実行を実施した結果を下記に示します。

バグ埋め込みプログラムへの適用結果

 

緑の四角で囲まれた箇所が誤って「追加」したバグが検出されたところです。

したがって、3種類のバグすべてが、本テストプロセスによって検出できることがわかりました。

現場に適用するにあたって

実験ではうまくいきましたが、実際の商用ソフトウェアではどうでしょうか。現場でこの手法を適用するためには、いくつかの大きな課題があります。

1つは、ツールによる依存性です。これまで説明したように、本手法ではシンボリック実行ツールを活用します。それゆえ、ツールの制約が本手法の制約になってしまいます。ツールによってはバイト配列や浮動小数点をサポートしていないなどの制約があり、適用のためにプログラムを修正するなどの工夫が必要です。

2つめは、大規模なソフトウェアへ適用時に課題となる、パス爆発と結果の比較量の増大です。前者は、シンボリック実行関連の研究テーマとして最もホットな領域です。プログラムにループが入ると、それほど規模が大きくなくても、パスの爆発、つまりコンピュータのメモリを現実的ではない容量使ってしまったり、CPUの演算が何日たっても終わらない状態となります。この課題に対しては、たとえば入力変数のうち独立と考えてもよい変数は組み合わせないことで、組み合わせの数を削減するという対策があります。後者については、従来の変更のプロセスを見直すことで改善できます。すなわち、一気に変更をしてから、変更前後の出力を比較するのではなく、部分的な変更と結果の比較を何度も繰り返しながら変更を進めるやりかたに変えます。テストケースが自動生成できるため、この方法は現実的な解となりえます。

3つめは、技法を使うためのスキルの問題です。いまフリーのツールがいろいろありますが、インストールや利用方法が複雑であったり、利用のためにはツールの一部を修正するなど、自分の環境に合わせてカスタマイズを試行錯誤する必要があります。また、日本にはユーザーコミュニティがないため、ノウハウや適用事例の共有が進まないことも、課題です。解決方法は、とにかく情報を共有し、事例を増やしていくことしかありません。このブログもその一助となれば幸いです。

なお、この考察の内容はIEEEの論文にも記載しております。ご興味あればどうぞ。。。