「モデルベーステスト」の版間の差分

削除された内容 追加された内容
Addbot (会話 | 投稿記録)
m ボット: 言語間リンク 8 件をウィキデータ上の d:q1399743 に転記
Melan (会話 | 投稿記録)
en:Model-based testing(2013年2月26日 12:37:04(UTC))の翻訳をマージ
9行目:
== モデル ==
特に[[モデル駆動工学]]や[[Object Management Group|OMG]]の[[モデル駆動型アーキテクチャ]]では、テスト対象システムの開発以前に(あるいは並行して)モデルが構築される。このモデルも完全なシステムから構築される。これまでモデル構築はほとんど人間が行っていたが、例えばソースコードからモデルを自動的に生成する試みもなされている。新たなモデルを生成する重要な方法の1つとして[[モデル変換言語]]や[[ドメイン固有言語]]を使った[[モデル変換]]がある。
 
=== モデル検査によるベーステストケース生成の使い方 ===
モデルベーステストの使い方はいくつかあり、「オンラインテスト」、「オフラインの実行可能テスト生成」、「オフラインの手動実行可能なテスト生成」などがある<ref name="pmbt">[http://www.cs.waikato.ac.nz/research/mbt/ ''Practical Model-Based Testing: A Tools Approach''], Mark Utting and Bruno Legeard, ISBN 978-0-12-372501-1, Morgan-Kaufmann 2007</ref>。
 
オンラインテストとは、対象システムとモデルベーステストのツールを直接接続し、動的にテストを行うものである。
 
オフラインの実行可能テスト生成とは、後で自動実行可能な形のテストケースを生成することをいう。例えば、生成されたテストロジックを[[Python]]のクラス群で実装する。
 
オフラインの手動実行可能なテスト生成とは、人間が読める形のテストを生成し、後でそれに従って人手でテストを行う。例えば、PDFなどの形式で人間が読める(自然言語で書かれた)テスト仕様書を生成する。
 
== アルゴリズム的なテスト導出 ==
モデルベーステストの主な有効性は、自動化の可能性にある。モデルを機械が読み取ることができ、十分に形式的であれば、基本的にテストケースを機械的に抽出することができるはずである。
 
=== 有限状態機械 ===
一般にモデルは[[有限オートマトン]]や[[状態遷移系]]に変換(翻訳)される。このオートマトンはテスト対象システムのとりうる構成を表現している。テストケースを探すには、このオートマトン上で実行可能経路を探す。1つの実行可能経路が1つのテストケースに対応することになる。この手法はモデルが[[決定性有限オートマトン|決定的]]であるか、決定的な形式に変換可能である場合にうまく機能する。
 
テスト対象システムが非常に複雑であった場合、システムのとりうる状態数が膨大となり、実行可能経路数も膨大となる可能性がある。適切なテストケースを見つけ出すには、例えば特定の証明すべき状況を指定して経路探索の補助とする。テストケースの選択には様々な手法が適用される<ref>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</ref>
 
=== 定理証明によるテストケース生成 ===
[[自動定理証明]]は本来、論理式の自動的な証明に使われるものであった。モデルベーステストでは、システムを一群の論理式でモデル化してシステムの振る舞いを記述する<ref name="otbt">{{Cite journal |first1=Achim D. |last1=Brucker |first2=Burkhart |last2=Wolff |title=On Theorem Prover-based Testing |journal=Formal Aspects of Computing |year=2012 |doi=10.1007/s00165-012-0222-y |url= http://www.brucker.ch/bibliography/abstract/brucker.ea-theorem-prover-2012.en.html}}</ref>。テストケースを選択するには、テスト対象システムを記述した論理式群を翻訳したものを[[同値]]なクラスで分類する。各クラスは特定のシステムの振る舞いを表現しており、テストケースと対応させることができる。
 
簡単な分類法として[[加法標準形]]を使った手法がある。システムの振る舞いを表す論理式を加法標準形に変換するのである。
24 ⟶ 34行目:
[[木構造 (データ構造)|木構造]]を使った分類で、さらに洗練された階層的な分類が可能となる。分類のアルゴリズムをサポートするヒューリスティックも利用できる。例えば[[限界値分析]]に基づいたヒューリスティックなどがある。
 
=== 制約論理プログラミングによるテストケース生成と記号的実行 ===
[[制約論理プログラミング]]では、変数群の制約条件を満足する解を求めることによって特定の制約を満たすテストケースを選択することができる。システムは制約によって記述される<ref>Jefferson Offutt. Constraint-Based Automatic Test Data Generation. IEEE Transactions on Software Engineering, 17:900-910, 1991</ref>。制約条件群は[[充足可能性問題]]を解くことで解が得られたり、[[ガウスの消去法]]のような[[数値解析]]によって解が得られる。制約条件式群を解くことで得られたものを対象システムのテストケースとして使用することができる。
 
[[制約プログラミング]]は記号的実行 (Symbolic Execution) と組み合わせることもできる。その場合、システムモデルを記号的に実行する。すなわち、異なる制御経路群についてデータ制約を集め、制約プログラミングの手法を使って制約を解き、テストケースを生成する<ref>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</ref>。
 
=== モデル検査 ===
本来、[[モデル検査]]はモデルが仕様を満足するかを検証する技法として開発された。モデルベーステストに応用する場合<ref>Gordon Fraser, Franz Wotawa, and Paul E. Ammann. [http://dl.acm.org/citation.cfm?id=1600261 Testing with model checkers: a survey]. Software Testing, Verification and Reliability, 19(3):215–261, 2009. </ref>、テスト対象システムのモデルとテストしたい属性をモデル検査機に与える。モデル検査機はその属性がモデル上で正しいかどうかを証明する過程で証拠と反例を検出する。証拠となる経路はその属性を満足する。一方、反例となる経路を実行すると、その属性に反した状態となる。これらの経路がテストケースとして使用できる。
 
=== 記号的実行マルコフ連鎖テストモデルによるテストケース生成 ===
[[マルコフ連鎖]]はモデルベーステストの効率的方法となる。マルコフ連鎖を実装したテストモデルは使い方のモデルとみることができる。使い方のあらゆるシナリオを表現した[[有限オートマトン]]と、そのシステムがどのように使われるかを統計的に表した運用プロファイルとで構成される。有限オートマトンは何ができるかを表現しており、テスト対象となる。運用プロファイルは運用テストケースの生成を助ける。この技法は、システムを網羅的にテストするのが困難で、そもそも問題(バグ)がほとんどないようなシステムのテストケースを生成するために生まれた<ref>Helene Le Guen. [ftp://ftp.irisa.fr/techreports/theses/2005/leguen.pdf Validation d'un logiciel par le test statistique d'usage : de la modelisation de la decision à la livraison], 2005. </ref>。そのため、テスト対象システムの信頼性向上を目的として統計的なテストケースを生成するのに適している。近年、組み込みシステムにも適用できるよう拡張されている<ref>http://www.amazon.de/Model-Based-Statistical-Continuous-Concurrent-Environment/dp/3843903484/ref=sr_1_1?ie=UTF8&qid=1334231267&sr=8-1</ref>。
 
== 脚注 ==
=== モデル検査によるテストケース生成 ===
{{Reflist}}
本来、[[モデル検査]]はモデルが仕様を満足するかを検証する技法として開発された。モデルベーステストに応用する場合、テスト対象システムのモデルとテストしたい属性をモデル検査機に与える。モデル検査機はその属性がモデル上で正しいかどうかを証明する過程で証拠と反例を検出する。証拠となる経路はその属性を満足する。一方、反例となる経路を実行すると、その属性に反した状態となる。これらの経路がテストケースとして使用できる。
 
== 参考文献 ==
=== 記号的実行によるテストケース生成 ===
*OMG UML 2 Testing Profile; [http://www.omg.org/spec/UTP/]
記号的実行(Symbolic Execution)をモデルベーステストのフレームワークとして利用することがある。これは抽象モデルでの実行経路を追跡する手段となる。基本的にプログラム実行を実際の値を使わずに、変数を記号として扱ってシミュレートする。各実行経路が可能なプログラム実行経路を表し、テストケースとして利用できる。その際に記号に値を設定してインスタンス化する。
*{{Cite conference | last1 = Bringmann | first1 = E. | last2 = Krämer | first2 = A. | doi = 10.1109/ICST.2008.45 | title = Model-Based Testing of Automotive Systems | booktitle = 2008 International Conference on Software Testing, Verification, and Validation | conference = International Conference on Software Testing, Verification, and Validation (ICST)| pages = 485–493 | year = 2008 | isbn = 978-0-7695-3127-4 | url = http://www.piketec.com/downloads/papers/Kraemer2008-Model_based_testing_of_automotive_systems.pdf }}
*[http://www.cs.waikato.ac.nz/research/mbt ''Practical Model-Based Testing: A Tools Approach''], Mark Utting and Bruno Legeard, ISBN 978-0-12-372501-1, Morgan-Kaufmann 2007.
*[http://www.cambridge.org/us/catalogue/catalogue.asp?isbn=9780521687614 ''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.
*[http://www.springer.com/west/home/computer/programming?SGWID=4-40007-22-52081580-detailsPage=ppmmedia%7CaboutThisBook ''Model-Based Testing of Reactive Systems''] Advanced Lecture Series, LNCS 3472, Springer-Verlag, 2005. ISBN 978-3-540-26278-7.
*{{Cite book | author = Hong Zhu et al. | title = AST '08: Proceedings of the 3rd International Workshop on Automation of Software Test | url = http://portal.acm.org/citation.cfm?id=1370042# | year = 2008 | publisher = ACM Press | isbn = 978-1-60558-030-2}}
*{{Cite conference | last1 = Santos-Neto | first1 = P. | last2 = Resende | first2 = R. | last3 = Pádua | first3 = C. | doi = 10.1145/1244002.1244306 | title = Requirements for information systems model-based testing | booktitle = Proceedings of the 2007 ACM symposium on Applied computing - SAC '07 | conference = Symposium on Applied Computing | pages = 1409–1415 | year = 2007 | isbn = 1-59593-480-4 }}
*{{Cite journal | last1 = Roodenrijs | first1 = E. | title = Model-Based Testing Adds Value | journal = Methods & Tools | volume = 18 | issue = 1 | pages = 33–39 | year = 2010 | month = Spring | issn = 1661-402X| url = http://www.methodsandtools.com/archive/archive.php?id=102}}
*[http://squall.sce.carleton.ca/pubs/tech_report/TR_SCE-10-04.pdf ''A Systematic Review of Model Based Testing Tool Support''], Muhammad Shafique, Yvan Labiche, Carleton University, Technical Report, May 2010.
*{{Cite book |editor1-last=Zander |editor1-first=Justyna |editor2-last=Schieferdecker |editor2-first=Ina |editor3-last=Mosterman |editor3-first=Pieter J. |title=Model-Based Testing for Embedded Systems |series=Computational Analysis, Synthesis, and Design of Dynamic Systems |volume=13 |year=2011 |publisher=CRC Press |location=Boca Raton |isbn=978-1-4398-1845-9}}
*[http://www.model-based-testing.orginfo modelOnline Community for Model-based testingTesting]
*[http://www.robertvbinder.com/docs/arts/MBT-User-Survey.pdf ''2011 Model-based Testing User Survey: Results and Analysis'' Robert V. Binder. System Verification Associates, February 2012]
 
== 関連項目 ==
* [[モデル駆動型アーキテクチャ]] (MDA)
* [[モデル駆動工学]] (MDE)
* [[ドメイン固有言語]] (DSL)
* [[ドメイン固有モデリング]] (DSM)
* [[オブジェクト指向分析設計]] (OOOOAD)
* [[メタモデル]]
* [[XML Metadata Interchange|XMI]]
* [[Object Constraint Language|OCL]]
* [[Meta-Object Facility|MOF]]
* [[オブジェクト指向]] (OO)
 
==外部リンク==
*[http://a-most.iese.fraunhofer.de the Annual Workshop on Advances in Model Based Testing]
*[http://www.model-based-testing.org model-based testing]
*[http://www.goldpractices.com/practices/mbt/index.php Model Based Testing] モデルベーステストの適用に関する調査
*[http://www.mdqa.org/ MDQA.org] MBTおよびモデル駆動型品質保証に関するサイト
;ツール:
*[http://research.microsoft.com/fse/asml/ AsmL Test Tool] AsmLモデルから直接テストを生成できる(マイクロソフト)
*[http://research.microsoft.com/specexplorer/ Spec Explorer] マイクロソフト
*[http://www.atyoursideconsulting.com/ ATD-Automated Test Designer] テストケース、テストデータ、テスト自動化スクリプトを要求仕様から生成するMBTツール
*[http://www.conformiq.com/qtronic.php Conformiq Qtronic] [[統一モデリング言語|UML]]と[[Java]]に対応したMBTツール
*[http://www.conformiq.com/ctg.php Conformiq Test Generator] UMLの状態遷移図でテスト戦略を表現したものからテストを実行するツール
*[http://www-list.cea.fr/labos/gb/LSL/test/gatel/index.html GATeL] SCADE/Lustre モデルからテストを自動生成するツール
*[http://www.brucker.ch/projects/hol-testgen/ HOL-TestGen] Isabelle theorem prover という対話型[[自動定理証明]]機に基づいたテストケース生成ツール
*[http://www.leiriossmartesting.com/index.php/cms/en/product/certify-it LeiriosSmartesting Test GeneratorCertifyIt] BPMN および UML 2.0 によるシステム仕様記述からテストを自動生成するツール
*[http://www-verimag.imag.fr/~synchron/index.php?page=lurette/lurette Lurette] Lustre 言語で書かれたプログラム用の自動テストツール
*[http://www-verimag.imag.fr/~async/TGV/index.shtml.en TGV] プロトコル用テスト生成ツール
*[http://cordis.europa.eu/data/PROJ_FP5/ACTIONeqDndSESSIONeq112422005919ndDOCeq1451ndTBLeqEN_PROJ.htm MaTeLo] マルコフ連鎖に基づいたシナリオベースの戦略的テストツール
*[http://www.reactive-systems.com/ Reactis Tester] [[制御システム]]向けのMBTツール
*[http://www.t-vec.com/solutions/simulink.php Simulink Tester] Simulink および Stateflow モデルを変換してモデル分析とテスト生成を行うツール
66 ⟶ 82行目:
*[http://fmt.cs.utwente.nl/tools/torx/introduction.html TorX]
 
[[Category{{DEFAULTSORT:ソフトウェアテスティング|もてるへすてすと]]}}
[[Category:ソフトウェアテスティング]]