モデルベーステスト（Model-besed testing）とは、テストケースの一部または全部を評価対象システムの（通常、機能的側面を）モデル化したものから導出して行うソフトウェアテストの手法である。モデルはテスト対象のシステムの実現すべき動作を表現した抽象的なものである。そのようなモデルから導出されるテストケースはモデルと同程度に抽象化された機能テストであり、直接実行することはできない。そのため、抽象的なテストケースを実行可能なテストケースに変換する必要がある。モデルからテストを導出する方法はいくつも存在する。ソフトウェアテストは実験的でヒューリスティックスに基づいているため、最善の方法というものは存在しない。一般に全てのテストに関連する設計上の決定をまとめ、パッケージ化する。これを「テスト要求仕様; test requirements」、「テスト目的; test purpose」、場合によっては「ユースケース」と呼ぶ。このパッケージにはテストの中心となるべき部分のモデルに関する情報が含まれ、テスト終了条件が記述される。モデルベーステストではテストスイートはソースコードからではなくモデルから抽出されるため、一種のブラックボックステストを構成するのが一般的である。見方によってはこれは完全とはいえない。モデルベーステストとソースコードレベルのテストの網羅率測定を組み合わせ、機能的モデルを初期段階のソースコードに基づいて構築するなどのテスト改善方法が考えられる。複雑なソフトウェアシステムのモデルベーステストは発展途上の分野である。特にモデル駆動工学やOMGのモデル駆動型アーキテクチャでは、テスト対象システムの開発以前に（あるいは並行して）モデルが構築される。このモデルも完全なシステムから構築される。これまでモデル構築はほとんど人間が行っていたが、例えばソースコードからモデルを自動的に生成する試みもなされている。新たなモデルを生成する重要な方法の1つとしてモデル変換言語やドメイン固有言語を使ったモデル変換がある。モデルベーステストの使い方はいくつかあり、「オンラインテスト」、「オフラインの実行可能テスト生成」、「オフラインの手動実行可能なテスト生成」などがある。オンラインテストとは、対象システムとモデルベーステストのツールを直接接続し、動的にテストを行うものである。オフラインの実行可能テスト生成とは、後で自動実行可能な形のテストケースを生成することをいう。例えば、生成されたテストロジックをPythonのクラス群で実装する。オフラインの手動実行可能なテスト生成とは、人間が読める形のテストを生成し、後でそれに従って人手でテストを行う。例えば、PDFなどの形式で人間が読める（自然言語で書かれた）テスト仕様書を生成する。モデルベーステストの主な有効性は、自動化の可能性にある。モデルを機械が読み取ることができ、十分に形式的であれば、基本的にテストケースを機械的に抽出することができるはずである。一般にモデルは有限オートマトンや状態遷移系に変換（翻訳）される。このオートマトンはテスト対象システムのとりうる構成を表現している。テストケースを探すには、このオートマトン上で実行可能経路を探す。1つの実行可能経路が1つのテストケースに対応することになる。この手法はモデルが決定的であるか、決定的な形式に変換可能である場合にうまく機能する。テスト対象システムが非常に複雑であった場合、システムのとりうる状態数が膨大となり、実行可能経路数も膨大となる可能性がある。適切なテストケースを見つけ出すには、例えば特定の証明すべき状況を指定して経路探索の補助とする。テストケースの選択には様々な手法が適用される。自動定理証明は本来、論理式の自動的な証明に使われるものであった。モデルベーステストでは、システムを一群の論理式でモデル化してシステムの振る舞いを記述する。テストケースを選択するには、テスト対象システムを記述した論理式群を翻訳したものを同値なクラスで分類する。各クラスは特定のシステムの振る舞いを表現しており、テストケースと対応させることができる。簡単な分類法として加法標準形を使った手法がある。システムの振る舞いを表す論理式を加法標準形に変換するのである。木構造を使った分類で、さらに洗練された階層的な分類が可能となる。分類のアルゴリズムをサポートするヒューリスティックも利用できる。例えば限界値分析に基づいたヒューリスティックなどがある。制約論理プログラミングでは、変数群の制約条件を満足する解を求めることによって特定の制約を満たすテストケースを選択することができる。システムは制約によって記述される。制約条件群は充足可能性問題を解くことで解が得られたり、ガウスの消去法のような数値解析によって解が得られる。制約条件式群を解くことで得られたものを対象システムのテストケースとして使用することができる。制約プログラミングは記号的実行 (Symbolic Execution) と組み合わせることもできる。その場合、システムモデルを記号的に実行する。すなわち、異なる制御経路群についてデータ制約を集め、制約プログラミングの手法を使って制約を解き、テストケースを生成する。本来、モデル検査はモデルが仕様を満足するかを検証する技法として開発された。モデルベーステストに応用する場合、テスト対象システムのモデルとテストしたい属性をモデル検査機に与える。モデル検査機はその属性がモデル上で正しいかどうかを証明する過程で証拠と反例を検出する。証拠となる経路はその属性を満足する。一方、反例となる経路を実行すると、その属性に反した状態となる。これらの経路がテストケースとして使用できる。マルコフ連鎖はモデルベーステストの効率的方法となる。マルコフ連鎖を実装したテストモデルは使い方のモデルとみることができる。使い方のあらゆるシナリオを表現した有限オートマトンと、そのシステムがどのように使われるかを統計的に表した運用プロファイルとで構成される。有限オートマトンは何ができるかを表現しており、テスト対象となる。運用プロファイルは運用テストケースの生成を助ける。この技法は、システムを網羅的にテストするのが困難で、そもそも問題（バグ）がほとんどないようなシステムのテストケースを生成するために生まれた。そのため、テスト対象システムの信頼性向上を目的として統計的なテストケースを生成するのに適している。近年、組み込みシステムにも適用できるよう拡張されている。

出典:wikipedia