モデルベーステスト

モデルベーステスト（Model-based testing）とは、テストケースの一部または全部を評価対象システムの（通常、機能的側面を）モデル化したものから導出して行うソフトウェアテストの手法である。モデルはテスト対象のシステムの実現すべき動作を表現した抽象的なものである。そのようなモデルから導出されるテストケースはモデルと同程度に抽象化された機能テストであり、直接実行することはできない。そのため、抽象的なテストケースを実行可能なテストケースに変換する必要がある。

モデルからテストを導出する方法はいくつも存在する。ソフトウェアテストは実験的でヒューリスティックスに基づいているため、最善の方法というものは存在しない。一般に全てのテストに関連する設計上の決定をまとめ、パッケージ化する。これを「テスト要求仕様; test requirements」、「テスト目的; test purpose」、場合によっては「ユースケース」と呼ぶ。このパッケージにはテストの中心となるべき部分のモデルに関する情報が含まれ、テスト終了条件が記述される。

モデルベーステストではテストスイートはソースコードからではなくモデルから抽出されるため、一種のブラックボックステストを構成するのが一般的である。見方によってはこれは完全とはいえない。モデルベーステストとソースコードレベルのテストの網羅率測定を組み合わせ、機能的モデルを初期段階のソースコードに基づいて構築するなどのテスト改善方法が考えられる。

複雑なソフトウェアシステムのモデルベーステストは発展途上の分野である。

モデル

特にモデル駆動工学やOMGのモデル駆動型アーキテクチャでは、テスト対象システムの開発以前に（あるいは並行して）モデルが構築される。このモデルも完全なシステムから構築される。これまでモデル構築はほとんど人間が行っていたが、例えばソースコードからモデルを自動的に生成する試みもなされている。新たなモデルを生成する重要な方法の1つとしてモデル変換言語やドメイン固有言語を使ったモデル変換がある。

モデルベーステストの使い方

モデルベーステストの使い方はいくつかあり、「オンラインテスト」、「オフラインの実行可能テスト生成」、「オフラインの手動実行可能なテスト生成」などがある^[1]。

オンラインテストとは、対象システムとモデルベーステストのツールを直接接続し、動的にテストを行うものである。

オフラインの実行可能テスト生成とは、後で自動実行可能な形のテストケースを生成することをいう。例えば、生成されたテストロジックをPythonのクラス群で実装する。

オフラインの手動実行可能なテスト生成とは、人間が読める形のテストを生成し、後でそれに従って人手でテストを行う。例えば、PDFなどの形式で人間が読める（自然言語で書かれた）テスト仕様書を生成する。

アルゴリズム的なテスト導出

モデルベーステストの主な有効性は、自動化の可能性にある。モデルを機械が読み取ることができ、十分に形式的であれば、基本的にテストケースを機械的に抽出することができるはずである。

有限状態機械

一般にモデルは有限オートマトンや状態遷移系に変換（翻訳）される。このオートマトンはテスト対象システムのとりうる構成を表現している。テストケースを探すには、このオートマトン上で実行可能経路を探す。1つの実行可能経路が1つのテストケースに対応することになる。この手法はモデルが決定的であるか、決定的な形式に変換可能である場合にうまく機能する。

テスト対象システムが非常に複雑であった場合、システムのとりうる状態数が膨大となり、実行可能経路数も膨大となる可能性がある。適切なテストケースを見つけ出すには、例えば特定の証明すべき状況を指定して経路探索の補助とする。テストケースの選択には様々な手法が適用される^[2]。

定理証明

自動定理証明は本来、論理式の自動的な証明に使われるものであった。モデルベーステストでは、システムを一群の論理式でモデル化してシステムの振る舞いを記述する^[3]。テストケースを選択するには、テスト対象システムを記述した論理式群を翻訳したものを同値なクラスで分類する。各クラスは特定のシステムの振る舞いを表現しており、テストケースと対応させることができる。

簡単な分類法として加法標準形を使った手法がある。システムの振る舞いを表す論理式を加法標準形に変換するのである。

木構造を使った分類で、さらに洗練された階層的な分類が可能となる。分類のアルゴリズムをサポートするヒューリスティックも利用できる。例えば限界値分析に基づいたヒューリスティックなどがある。

制約論理プログラミングと記号的実行

制約論理プログラミングでは、変数群の制約条件を満足する解を求めることによって特定の制約を満たすテストケースを選択することができる。システムは制約によって記述される^[4]。制約条件群は充足可能性問題を解くことで解が得られたり、ガウスの消去法のような数値解析によって解が得られる。制約条件式群を解くことで得られたものを対象システムのテストケースとして使用することができる。

制約プログラミングは記号的実行 (Symbolic Execution) と組み合わせることもできる。その場合、システムモデルを記号的に実行する。すなわち、異なる制御経路群についてデータ制約を集め、制約プログラミングの手法を使って制約を解き、テストケースを生成する^[5]。

モデル検査

本来、モデル検査はモデルが仕様を満足するかを検証する技法として開発された。モデルベーステストに応用する場合^[6]、テスト対象システムのモデルとテストしたい属性をモデル検査機に与える。モデル検査機はその属性がモデル上で正しいかどうかを証明する過程で証拠と反例を検出する。証拠となる経路はその属性を満足する。一方、反例となる経路を実行すると、その属性に反した状態となる。これらの経路がテストケースとして使用できる。

マルコフ連鎖テストモデルによるテストケース生成

マルコフ連鎖はモデルベーステストの効率的方法となる。マルコフ連鎖を実装したテストモデルは使い方のモデルとみることができる。使い方のあらゆるシナリオを表現した有限オートマトンと、そのシステムがどのように使われるかを統計的に表した運用プロファイルとで構成される。有限オートマトンは何ができるかを表現しており、テスト対象となる。運用プロファイルは運用テストケースの生成を助ける。この技法は、システムを網羅的にテストするのが困難で、そもそも問題（バグ）がほとんどないようなシステムのテストケースを生成するために生まれた^[7]。そのため、テスト対象システムの信頼性向上を目的として統計的なテストケースを生成するのに適している。近年、組み込みシステムにも適用できるよう拡張されている^[8]。

出典

^ Practical Model-Based Testing: A Tools Approach, Mark Utting and Bruno Legeard, ISBN 978-0-12-372501-1, Morgan-Kaufmann 2007
^ John Rushby. Automated Test Generation and Verified Software. Verified Software: Theories, Tools, Experiments: First IFIP TC 2/WG 2.3 Conference, VSTTE 2005, Zurich, Switzerland, October 10–13. pp. 161-172, Springer-Verlag
^ Brucker, Achim D.; Wolff, Burkhart (2012). “On Theorem Prover-based Testing”. Formal Aspects of Computing. doi:10.1007/s00165-012-0222-y.
^ Jefferson Offutt. Constraint-Based Automatic Test Data Generation. IEEE Transactions on Software Engineering, 17:900-910, 1991
^ Antti Huima. Implementing Conformiq Qtronic. Testing of Software and Communicating Systems, Lecture Notes in Computer Science, 2007, Volume 4581/2007, 1-12, DOI: 10.1007/978-3-540-73066-8_1
^ Gordon Fraser, Franz Wotawa, and Paul E. Ammann. Testing with model checkers: a survey. Software Testing, Verification and Reliability, 19(3):215–261, 2009.
^ Helene Le Guen. Validation d'un logiciel par le test statistique d'usage : de la modelisation de la decision à la livraison, 2005.
^ ASIN 3843903484

参考文献

OMG UML 2 Testing Profile; [1]
Bringmann, E.; Krämer, A. (2008). "Model-Based Testing of Automotive Systems" (PDF). 2008 International Conference on Software Testing, Verification, and Validation. International Conference on Software Testing, Verification, and Validation (ICST). pp. 485–493. doi:10.1109/ICST.2008.45. ISBN 978-0-7695-3127-4。
Practical Model-Based Testing: A Tools Approach, Mark Utting and Bruno Legeard, ISBN 978-0-12-372501-1, Morgan-Kaufmann 2007.
Model-Based Software Testing and Analysis with C#, Jonathan Jacky, Margus Veanes, Colin Campbell, and Wolfram Schulte, ISBN 978-0-521-68761-4, Cambridge University Press 2008.
Model-Based Testing of Reactive Systems Advanced Lecture Series, LNCS 3472, Springer-Verlag, 2005. ISBN 978-3-540-26278-7.
Hong Zhu et al. (2008). AST '08: Proceedings of the 3rd International Workshop on Automation of Software Test. ACM Press. ISBN 978-1-60558-030-2
Santos-Neto, P.; Resende, R.; Pádua, C. (2007). "Requirements for information systems model-based testing". Proceedings of the 2007 ACM symposium on Applied computing - SAC '07. Symposium on Applied Computing. pp. 1409–1415. doi:10.1145/1244002.1244306. ISBN 1-59593-480-4。
Roodenrijs, E. (Spring 2010). “Model-Based Testing Adds Value”. Methods & Tools 18 (1): 33–39. ISSN 1661-402X.
A Systematic Review of Model Based Testing Tool Support, Muhammad Shafique, Yvan Labiche, Carleton University, Technical Report, May 2010.
Zander, Justyna; Schieferdecker, Ina; Mosterman, Pieter J., eds (2011). Model-Based Testing for Embedded Systems. Computational Analysis, Synthesis, and Design of Dynamic Systems. 13. Boca Raton: CRC Press. ISBN 978-1-4398-1845-9
Online Community for Model-based Testing
2011 Model-based Testing User Survey: Results and Analysis Robert V. Binder. System Verification Associates, February 2012

外部リンク

the Annual Workshop on Advances in Model Based Testing

ツール

Spec Explorer マイクロソフト
ATD-Automated Test Designer テストケース、テストデータ、テスト自動化スクリプトを要求仕様から生成するMBTツール
HOL-TestGen Isabelle theorem prover という対話型自動定理証明機に基づいたテストケース生成ツール
MaTeLo
Smartesting CertifyIt BPMN および UML 2.0 によるシステム仕様記述からテストを自動生成するツール
TGV プロトコル用テスト生成ツール
Reactis Tester 制御システム向けのMBTツール
Simulink Tester Simulink および Stateflow モデルを変換してモデル分析とテスト生成を行うツール
T-VEC Tabular Modeler
TorX

[pmbt-1] Practical Model-Based Testing: A Tools Approach, Mark Utting and Bruno Legeard, ISBN 978-0-12-372501-1, Morgan-Kaufmann 2007

[2] John Rushby. Automated Test Generation and Verified Software. Verified Software: Theories, Tools, Experiments: First IFIP TC 2/WG 2.3 Conference, VSTTE 2005, Zurich, Switzerland, October 10–13. pp. 161-172, Springer-Verlag

[otbt-3] Brucker, Achim D.; Wolff, Burkhart (2012). “On Theorem Prover-based Testing”. Formal Aspects of Computing. doi:10.1007/s00165-012-0222-y.

[4] Jefferson Offutt. Constraint-Based Automatic Test Data Generation. IEEE Transactions on Software Engineering, 17:900-910, 1991

[5] Antti Huima. Implementing Conformiq Qtronic. Testing of Software and Communicating Systems, Lecture Notes in Computer Science, 2007, Volume 4581/2007, 1-12, DOI: 10.1007/978-3-540-73066-8_1

[6] Gordon Fraser, Franz Wotawa, and Paul E. Ammann. Testing with model checkers: a survey. Software Testing, Verification and Reliability, 19(3):215–261, 2009.

[7] Helene Le Guen. Validation d'un logiciel par le test statistique d'usage : de la modelisation de la decision à la livraison, 2005.

[8] ASIN 3843903484

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]