モデル検査を用いたテストスイート生成について

考察

モデル検査を用いたテストスイート生成の基本的なアイデアは，望まれるシステムの性質に否定をつけてモデル検査を適用すると，反例として出てくるものは望まれるシステムの性質を検査するためのテストスイートになっているというものである．こうした望まれるシステムの性質のことをTest Purpose （テスト目的）といい，これらは自相論理式などで記述される．
そのテスト目的を否定化したものを「Negative Claim（否定的主張）」といい，それをモデル検査に意図的に用いるという意味で「Trap Property（策略性質）」などとも呼ばれる．（Testing with model checkers: A survey　他を参照）

さらに，Software Testing にはカバレッジという重要な概念がある．これは検査する Software のどの程度を用意されたテストスイートがカバーしたかの基準になるもので，通常パーセンテージで表示される．またカバレッジにはいくつかの概念があり，例えば次のような代表的なものが有る：ステートメントカバレッジ，エッジカバレッジ，コンディションカバレッジ，エッジ・コンディションカバレッジ，マルチプルカバレッジ，パスカバレッジ（Software Reliability methods, D. Peled, Springer より）つまりこれらは異なる基準概念のソフトウェアのカバレッジを規定するものであり，どのカバレッジの基準を開発しているソフトウェアに適用するかは場合によりけりである．

さて，最初の段落で，モデル検査を用いたテストスイート生成の基本的なアイデアとして，「望まれるシステムの性質に否定をつけてモデル検査を適用すると，反例として出てくるものは望まれるシステムの性質を検査するためのテストスイートになっているというもの」とした．またテスティングにおいてどのカバレッジを基準に用いるかかで用意するテストスイートも変わることも説明した．こうしたいくつかのカバレッジ基準に順ずるテストスイーツの生成はどのようにトラップ性質を作成するかによってコントロールする試みがなされている．つまり，トラップケースの作り方，つまり，望まれる性質の否定をとる方法にもいくつかのやり方があり，そのやり方によって，どのテストカバレッジの基準を目的にテストスイートを生成されるかがかわるのである．

ちなみに，テストケースの集合をテストスイートというのだそうだ．