各種検証技術の比較と使い分け

Requirements-basedテストモデルチェックによる形式検証フォーマルテストは要求に基づいたテスト・検証を行うという目的は共通です。この中で要求に基づいた検証を目的として最も広く使われている技法はRequirements-basedテストです。

Requirements-basedテストは非常に柔軟性が高く、利便性は高いものの、質の高いテストを目指すには大きな工数を要するという点が短所です。

モデルチェックによる形式検証も同様に、要求に基づいた検証を目的として利用されます。この検証技法は要求さえ形式化してしまえば、テストケースなどを記述する必要はなく、検証対象のソフトウェアをどれだけ長時間実行したとしても、ありとあらゆる入力値とその組み合わせが要求違反にならないことを完全に証明できることから、検証の質と工数の観点では最高位に位置します。しかし一方で、検証対象を完全に解析可能な表記でツールに提供しなければならない、大規模なソフトウェアの検証には長時間の解析を要する、などの制約があり、柔軟性には欠けます。

Requirements-basedテストとモデルチェックによる形式検証の間を取った技法がフォーマルテストです。

Requirements-basedテスト フォーマルテスト モデルチェックによる形式検証
テスト・検証対象

ブラックボックス可

ブラックボックス可 完全に解析可能な表記が必要
適用可能な規模

シミュレーション可能な規模

シミュレーション可能な規模 ソフトウェアユニット程度の規模
検証の完全性

テストケースを書いた分だけ

シミュレーションした全て ありとあらゆる実行 (完全)
テストケースの作成

全て手動

入力値と出力値(期待値)が必要

手動もしくは自動

入力値のみが必要

作成不要
柔軟性

テストケースとして書ければ評価可能

主に機能要求に関する判定に限られる 主に機能要求に関する判定に限られる
テストケースと要求の対応関係

手動でリンク

目視で確認

自動でリンク

自動で確認(テスト漏れも自動検出)

リンク不要

確認不要

 

どの検証手法を選べば良いか?

Requirements-basedテストモデルチェックによる形式検証フォーマルテストは要求に基づいたテスト・検証を行うという目的は共通ですが、前述の通りいずれも長所短所があるため、一概にどれが優れているとは言えません。

どれかを選択するよりも、用途に合わせて使い分けることの方が重要です。一つの開発プロセス上でも適切に組み合わせて利用することによって効率的かつ効果的なテストプロセスを構築することが可能になります。例えば、ソフトウェアユニットレベルであれば、モデルチェックによる形式検証を用いて完全な検証を行い、その確実に要求を守るソフトウェアユニット群の組み合わせで構成されるソフトウェアインテグレーションレベルとシステムレベルではフォーマルテストを用います。これらのテクノロジが得意としないような評価項目、例えば波形の形状などを評価する場合にはRequirements-basedテストで補完します。

 

特筆すべき点は、Requirements-basedテスト、モデルチェックによる形式検証、フォーマルテストを全て利用するとしても、ユーザの方が追加で覚えなければならない操作はそれほど多くは無いことです。テストケースの書き方、構造カバレッジの読み方はRequirements-basedテストとフォーマルテストで共通です。要求の形式化の方法はモデルチェックによる形式検証とフォーマルテストで共通です。要求カバレッジの読み方だけはフォーマルテスト特有ですが難解なものではありません。