Home Publications Curriculum Vitae Education

Model-based testing (MBT)

Testing is an essential, but time and resource consuming activity in the software development process. Generating a short, but effective test suite usually needs a lot of manual work and expert knowledge. In a model-based process, among other subtasks, test construction and test execution can also be partially automated.

Introduction
MBT tools and projects
Our test generation tool
References

Introduction to model-based test generation

The basic idea is that from a formal or semi-formal model (e.g. transition system, UML State Machines, class diagrams extended with constraints, etc.) complete test cases (input and expected output pairs) can be generated. There is an extensive research in this field, but the technology has matured enough that nowadays there are commercial tools and industrial applications.

This paper offers a good introduction to the topic:

Utting, M., Pretschner, A., Legeard, B.: A taxonomy of model-based testing. Technical Report ISSN 1170-487X, The University of Waikato (april 2006)
[it is now available as a journal paper in Software Testing, Verification and Reliability, doi: 10.1002/stvr.456]
Useful surveys in the field of model-based testing: Further information can be found in these two books:

MBT tools and projects

A far from complete list of MBT tools (last modification was checked on 2010.09.).
(If you know about an MBT tool that is not in the list, feel free to send me an email.)
(Note: some of these tools start from source code, thus they are strictly speaking not model-based tools, but they provide automatic test generation, so I included them in the list.)

Tool Modified Ref. Input format Description
AETG 2007 31 custom (AETGSpec textual notation) AETG is implemented as a web application to generate tests from requirements using pairwise coverage.
AutoTest 2010 34 Eiffel source code AutoTest uses assertions in Design by Contract to generate test cases. It automates test creation, test minimization. It is now integrated into the EiffelStudio IDE.
Conformiq Designer 2010 6 UML State Machines, QML Commercial tool implemented in Eclipse. Models can be created as UML State Machines and in Qtronic Modeling Language (QML). Tests can be exported to test management tools or TTCN-3. (Previously was Conformiq Qtronic.)
Cow_Suite 2003 33 UML Use Case and Sequence Diagrams Cow_Suite generates test cases from UML models according to structural coverage criteria.
CREST 2010 7 C source code CREST is an automatic test generation tool for C. It instruments the source code to perform symbolic execution, and uses a constraint solver to search for unexplored program paths.
CUTE 2006 8 C, Java source code A concolic unit testing engine for C and Java, similar to CREST. Can also handle concurrent programs.
DOTgEAr 2007 9 Java source Dataflow-oriented Test Case Generation for Object-oriented Software Systems by Evolutionary Algorithm
DSD-Crasher 2007 14 Java source DSD-Crasher is the successor of JCrasher. It adds two steps before the test generation: runs existing tests to capture their behaviour, then uses static analysis to explore the paths of the program.
Euclide 2009 10 C source Test generator for C, implemented as a web application. Uses contraint solvers to generate a test reaching a given point in the program.
GATeL 2004 11 Lustre LUSTRE is a declarative synchronous data-flow language. GATeL uses constraint solving techniques to generate test cases. Generation can be directed by test purposes or coverage criteria.
GUITAR 2010 12 GUI application (JFC, Windows) GUI Testing frAmewoRk: "rips" the GUI of an application and creates an event-flow graph model from it. GUITAR is open-source, there is a lot of publications and case studies with it.
JCrasher 2007 13 Java source JCrasher is an automatic robustness tester for Java. JCrasher examines the type information of a set of Java classes and constructs code fragments that will create instances of different types to test the behavior of public methods under random data.
JET 2008 15 Java code annotated with JML JET is an automated unit testing tool for Java classes annotated with Java Modeling Language (JML) specifications. It generates random tests and uses the JML constraints as test oracles.td>
JUMBL ? 16 Markov chains Java Usage Model Builder Library (JUMBL) is a set of command-line and GUI tools supporting automated, model-based, statistical testing of systems.
Korat 2007 36 Java code Korat is a tool for constraint-based generation of structurally complex test inputs for Java programs. Korat requires (1) an imperative predicate that specifies the desired structural constraints and (2) a finitization that bounds the desired test input size.
MaTeLo 2009 17 Markov chains MaTeLo (Markov Test Logic) is a commercial product to generate functional test cases. Strategies: random generation oriented by profiles, all transitions coverage. Can be connected to numerous test platforms.
mbt 2010   FSM Test generation from Finite State Machines. Search algoritms: A* or random, with a limit for various coverage criteria (state, edge, requirement).
MOTES 2010 18 EFSM MOTES generates tests from EFSM models in the form of TTCN-3 test cases. For offline test generation it uses the UPPAAL model checker, and there is an on-the-fly generator. The product is now called Elvior TestCast Generator.
NModel 2009 19 model program written in C# NModel is a model-based testing and analysis framework for model programs written in C#. Generation can be online or offline, it can be directed by a scenario. For offline generation the default strategy is link coverage, but it can be extended.
PathCrawler 2004 20 C source PathCrawler is a method to automatically generate path tests for the all-feasible-paths criterion with a user-defined limit on the number of loop iterations in the covered path.
Pex 2010 21 .NET program code With Pex testers create parametrized unit tests and then Pex finds input parameters for these test that result in high coverage, boundary conditions, exceptions and assertion failures. Pex applies dynamic symbolic execution and an underlying constraint solver.
PyModel 2010 35 Python source PyModel supports offline and on-the-fly testing. It uses composition for scenario control. Coverage can be guided by a programmable strategy.
SAL-ATG 2006 3 custom (transition system) Test generation using the SAL (Symbolic Analysis Laboratory) model checker at SRI International. State-of-the-art tools, many optimization technique implemented which are useful for test generation, like bounded model checking
SCOOTER 2005 32 UML Collaboration diagrams SCOOTER builds an intermediate model called SCOTEM from UML collaboration diagrams and state machines, and generates tests from it according to varios control-flow criteria.
Spec Explorer 2010 22 model programs in C# Spec Explorer 2010 is the successor of the AsmL Test Tool and Spec Explorer 2004, and is now moved to MSDN Dev Labs and is integrated into Visual Studio. The models can be written in C#, and test generation is directed with test purposes written in the Cord language.
STG 2007 23 NTIF (IOLTS) STG generates tests for IOLTS with the help of specified test purposes. The generation is black-box, state space explosion is prevented by symbolic generation. STG is implemented in Ocaml.
TAO 2004   C source TAO can generate test cases based on structural coverage, or from pre- and postconditions (with the CAVEAT tool).
Test Designer 2010 24 UML + OCL Test Designer is the successor of BZ-Testing-Tools and Leiros Test Generator, and now is a commercial product from Smartesting. The SUT is given with UML models enriched with OCL constraints, the tool generates tests to satisfy various model coverage criteria.
TestOptimal 2011   (E)FSM TestOptimal supports FSM and E-FSM modeling with several test case generation algorithms. It has various plugins for online testing web application, windows applications, database and web services, etc. It also supports data-driven testing and pair-wise algorithms right within the model and has the facility for performing load testing using the same models.
TGV 2004 25 LOTOS / IOLTS TGV allows the generation of an abstract test case from a specification and a test purpose. The generation is done "on-the-fly" on the synchronous product of the specification with the test purpose.
TorX 2008 26 LTS / LOTOS TorX is an automated tool for conformance testing. TorX generates the tests on-the-fly using a random strategy, which can be constrained by test purposes.
TTmodeler 2009 27 UML (UML 2 Testing Profile) TTmodeler is a plugin for TTworkbench, it can create TTCN-3 tests from UML models using the UML 2 Testing Profile.
T-VEC 2009   Simulink T-VEC Tester for Simulink and Stateflow generates test cases for MatthWorks Simulink models based on various structural coverage criteria.
UPPAAL Cover 2010 28 timed automata COVER is test-case generation tool for timed systems.It generates test cases from a timed automata model of a system to be tested, and a coverage criteria expressed in an observer language.
UPPAAL TRON 2009 28 timed automata UPAAL for Testing Realtime System ONline generates test suites on-the-fly with timing information for conformance testing.

Case studies:

Case study Year Ref. Description
GSM 11-11 2004 29 The case study presented generating test cases for a fragment of the Smart Card GSM 11-11 standard. From a B specification approximately 1000 test cases were generated. The effectiveness of the tests were compared to a manually created test suite.
Windows Protocol Documentation 2008-2009 30 The quality of the documentation of 220 protocols (22000 pages of specification, 36000 testable requirements) from Microsoft was tested using MBT methods. The project used the Spec Explorer tool. A 42% of efficiency gain was reported over the part of the project, which used manual test creation.

Various academic and industrial research projects on the topic:

Project Year Ref. Description
AGEDIS 2001-2004 2 Automated Generation and Execution of Test Suites for DIstributed Component-based Software: 3-year European Commission research project coordinated by IBM Research. Developed a framework, tools and conducted case studies. This paper is a good overview, a report about other test generator tools, the project final report and slides with the results and the lessons learnt. The deliverables of the projects can be used with an academic license.
MOGENTES 2008-2010   MOGENTES is an EU research project for improving testing of embedded systesm using MBT approaches. The project creates technologies for generating tests from UML and Simulink models using model checkers.
D-MINT 2007-2009   D-MINT (Deployment of Model-Based Technologies to Industrial Testing) is a three-year project with several industrial and academic partners. One of the main goals of the project is to apply MBT approaches to many deminstrators from automotive, manufacturing and telecommunication domains.

Relevant conferences:

Our test generation tool

We developed a test generation tool for UML statecharts that uses the SPIN model checker to traverse the state space and find test satisfying the test criteria. It has a Java GUI, which collects the user input, transforms the criterion (all state or all transition coverage) to LTL formulae, calls SPIN with the necessary parameters and creates XML test cases from the output of SPIN. The efficiency of the test generation was measured, different model checker options was compared. The optimal parameter set was tested in a real life statechart (with 31 states and 174 transitions).

Later the tool chain was extended to support broader part of the testing process:

The test generator creates abstract test files, i.e. defined with the events of the model. When an implementation is tested with them, the test cases and the method to apply them should be transformed to implementation-specific ones.

In a simple case study (with a statechart of a mobile phone) the abstract tests were transformed to JUnit tests. The tests covered more than 90% of the statements in the implementation, thus proved to be a useful method to create test cases.

Details:

References

  1. www.model-based-testing.org - a site created by Harry Robinson. Not maintained any more, but there are a lot of links to publications.
  2. A. Hartman and K. Nagin, "The AGEDIS tools for model based testing," SIGSOFT Softw. Eng. Notes, vol. 29, 2004, pp. 129-132., http://portal.acm.org/citation.cfm?id=1007529
  3. Grégoire Hamon, Leonardo de Moura, and John Rushby, "Automated Test Generation with SAL", CSL Technical Note, January 2005, http://www.csl.sri.com/users/rushby/abstracts/sal-atg
  4. Automatic Test Generation from Formal Specifications at NIST by Ammann and Black. Lot of useful papers, e.g. using mutation techniques and model checkers.
  5. Hyoung Seok Hong, Insup Lee, Oleg Sokolsky, Sung Deok Cha: Automatic Test Generation from Statecharts Using Model Checking, Technical Report MS-CIS-01-07, Feb 2001. http://www.cis.upenn.edu/~rtg/testgen/
  6. A. Huima, "Implementing Conformiq Qtronic," Testing of Software and Communicating Systems, Springer, 2007, pp. 1-12.
  7. J. Burnim and K. Sen, "Heuristics for Scalable Dynamic Test Generation," Automated Software Engineering, 2008. ASE 2008. 23rd IEEE/ACM International Conference on, 2008, pp. 443-446.
  8. K. Sen and G. Agha, "CUTE and jCUTE : Concolic Unit Testing and Explicit Path Model-Checking Tools," in 18th International Conference on Computer Aided Verification (CAV'06), Lecture Notes in Computer Science, Seattle, Washington, USA, August 2006. Springer.
  9. N. Oster and F. Saglietti, "Automatic Test Data Generation by Multi-objective Optimisation," Computer Safety, Reliability, and Security, 2006, pp. 426-438.
  10. Arnaud Gotlieb. EUCLIDE: A Constraint-Based Testing platform for critical C programs. In proceedings of 2th International Conference on Software Testing, Validation and Verification (ICST'09), April 2009
  11. Bruno Marre, Benjamin Blanc, Test Selection Strategies for Lustre Descriptions in GATeL, Electronic Notes in Theoretical Computer Science, Volume 111, Proceedings of the Workshop on Model Based Testing (MBT 2004), 1 January 2005, Pages 93-111, ISSN 1571-0661, DOI: 10.1016/j.entcs.2004.12.010. (http://www.sciencedirect.com/science/article/B75H1-4F6D1S9-7/2/27655df6ca1d89a201627f880becf45c)
  12. Daniel Hackner and Atif M. Memon. "Test Case Generator for GUITAR" In ICSE '08: Research Demonstration Track: International Conference on Software Engineering, (Washington, DC, USA), 2008.
  13. Christoph Csallner and Yannis Smaragdakis. "JCrasher: An automatic robustness tester for Java," Software -- Practice & Experience, vol. 34, no. 11, Sep. 2004, pp. 1025-1050. http://ranger.uta.edu/~csallner/papers/csallner04jcrasher-abstract.html
  14. Yannis Smaragdakis and Christoph Csallner. "Combining static and dynamic reasoning for bug detection" In Proc. International Conference on Tests And Proofs (TAP), Feb. 2007, pp. 1-16. http://ranger.uta.edu/~csallner/papers/smaragdakis07combining-abstract.html
  15. Yoonsik Cheon and Carlos E. Rubio-Medrano. Random Test Data Generation for Java Classes Annotated with JML Specifications. In Proceedings of the 2007 International Conference on Software Engineering Research and Practice, Volume II, June 25--28, 2007, Las Vegas, Nevada, pages 385-392.
  16. S.J. Prowell, "JUMBL: A Tool for Model-Based Statistical Testing," Proceedings of the 36th Annual Hawaii International Conference on System Sciences (HICSS'03) - Track 9 - Volume 9, IEEE Computer Society, 2003, p. 337.3.
  17. W. Dulz and Fenhua Zhen, "MaTeLo - statistical usage testing by annotated sequence diagrams, Markov chains and TTCN-3," Quality Software, 2003. Proceedings. Third International Conference on, 2003, pp. 336-342.
  18. J. Ernits, A. Kull, K. Raiend, and J. Vain, "Generating Tests from EFSM Models Using Guided Model Checking and Iterated Search Refinement," Formal Approaches to Software Testing and Runtime Verification, Springer, 2006, pp. 85-99. http://www.springerlink.com/content/b63737j0u97w3337/
  19. J. Jacky, M. Veanes, C. Campbell, and W. Schulte, Model-Based Software Testing and Analysis with C#, Cambridge University Press, 2007.
  20. N. Williams, B. Marre and P. Mouy. "Interleaving Static and Dynamic Analyses to Generate Path Tests for C Functions," 3rd Workshop on System Testing and Validation (SV'04), December 2004, Paris, France
  21. N. Tillmann and J. de Halleux, "Pex -- White Box Test Generation for .NET," Tests and Proofs, Springer, 2008, pp. 134-153. http://dx.doi.org/10.1007/978-3-540-79124-9_10
  22. M. Veanes, C. Campbell, W. Grieskamp, W. Schulte, N. Tillmann, and L. Nachmanson, "Model-Based Testing of Object-Oriented Reactive Systems with Spec Explorer," Formal Methods and Testing, Springer, 2008, pp. 39-76.
  23. D. Clarke, T. Jéron, V. Rusu, and E. Zinovieva, "STG: A Symbolic Test Generation Tool," Tools and Algorithms for the Construction and Analysis of Systems, Springer, 2002, pp. 151-173.
  24. F. Bouquet, C. Grandpierre, B. Legeard, and F. Peureux, "A test generation solution to automate software testing," Proceedings of the 3rd international workshop on Automation of software test, Leipzig, Germany: ACM, 2008, pp. 45-48.
  25. C. Jard and T. Jéron, "TGV: theory, principles and algorithms," International Journal on Software Tools for Technology Transfer (STTT), vol. 7, 2005, pp. 297-315.
  26. Tretmans, G.J. and Brinksma, H. TorX: Automated Model-Based Testing. In: First European Conference on Model-Driven Software Engineering, December 11-12, 2003, Nuremberg, Germany. pp. 31-43
  27. Stephan Pietsch, Bogdan Stanca-Kaposta. "Model-based testing with UTP and TTCN-3 and its application to HL7," Technical report, Testing Technologies IST GmbH. URL: http://testingtech.com/download/publications/ModelBasedTesting_Conquest08.pdf
  28. A. Hessel, K. Larsen, M. Mikucionis, B. Nielsen, P. Pettersson, and A. Skou, "Testing Real-Time Systems Using UPPAAL," Formal Methods and Testing, 2008, pp. 77-117. http://www.springerlink.com/content/7477540152576173/
  29. E. Bernard, B. Legeard, X. Luck, and F. Peureux, "Generation of test sequences from formal specifications: GSM 11-11 standard case study," Software: Practice and Experience, vol. 34, 2004, pp. 915-948.
  30. Grieskamp, W., Kicillof, N., Stobie, K. and Braberman, V. (2011), Model-based quality assurance of protocol documentation: tools and methodology. Software Testing, Verification and Reliability, 21: 55-71. DOI: 10.1002/stvr.427
  31. S. Dalal, A. Jain, N. Karunanithi, J. Leaton, C. Lott, G. Patton, and B. Horowitz, "Model-based testing in practice," Software Engineering, 1999. Proceedings of the 1999 International Conference on, 1999, pp. 285-294. http://doi.ieeecomputersociety.org/10.1109/ICSE.1999.841019
  32. S. Ali, L.C. Briand, M.J. Rehman, H. Asghar, M.Z.Z. Iqbal, and A. Nadeem, "A state-based approach to integration testing based on UML models," Information and Software Technology, vol. 49, Nov. 2007, pp. 1087-1106.
  33. F. Basanieri, A. Bertolino, E. Marchetti, "The Cow_Suite Approach to Planning and Deriving Test Suites in UML Projects", Proc. Fifth International Conference on the Unified Modeling Language - the Language and its applications UML 2002, LNCS 2460, Dresden, Germany, September 30 - October 4, 2002, p. 383-397.
  34. B. Meyer, A. Fiva, I. Ciupa, A. Leitner, Yi Wei, and E. Stapf, "Programs That Test Themselves," Computer, vol. 42, 2009, pp. 46-55.
  35. Jonathan Jacky, "PyModel: Model-based testing in Python", Northwest Python Day 2010, http://www.seapig.org/NWPD10Talks#PyModel
  36. C. Boyapati, S. Khurshid, and D. Marinov. Korat: Automated testing based on Java predicates, International Symposium on Software Testing and Analysis (ISSTA 2002), pages 123-133, Rome, Italy, July 2002

 

Last modified: 2011. 10. 21.