Home Publications CV 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 ofmanual work and expert knowledge. In a model-based process, among other subtasks, test construction and test execution can also be partially automated.

Note: these methods and tools require the creation of a model for the system under test, for methods that start from the source code see this list.


MBT tools

Projects and conferences


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. STVR 22:5, 2012. [previous version appeared as a tech report of The University of Waikato (April 2006)]

ISTQB prepared a Model-Based Tester extension to their certification scheme, their syllabus offers also a good overview of the topic.

ISTQB. ISTQB Foundation Level Certified Model-Based Tester. Version 2015.

MBT User Survey: survey results from practicioners reporting their experiences with MBT

MBT User Survey 2016, 2014, 2011
Useful surveys in the field of model-based testing: Further information can be found in these books:

MBT tools

A far from complete list of MBT tools (last modification was checked on 2014.07.).
(If you know about an MBT tool that is not in the list, feel free to send me an email.)

Tool Modified Ref. Input format Type Description
4Test 2016 Custom (Gherkin based) Commercial + Free version 4Test uses a combinatorial approach called constraint driven testing to select test cases from textual models specified in a syntax inspired by the Gherkin language.
BPM-Xchange 2014 [FS14] BPMN, UML... Commercial BPM-Xchange creates test cases from business process models based on different criteria (statement, branch, path, condition). It can import models from several modeling tools, and can export test cases to Excel, HP Quality Center, etc.
Conformiq Creator 2016 Activity Diagrams, DSL Commercial Creator uses a custom modeling language which is based on activity diagrams and a graphical domain specific action language. Models can be created via import from existing assets (e.g., flowcharts, BPM, Gherkin and manual tests), requirements can be downloaded from RMT, and generated tests can be exported to ALM tools, Excel, various scripting languages, or test execution with Conformiq Transformer.
Conformiq Designer 2014 [H07] UML State Machines, QML Commercial 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.)
DTM 2013 custom activity model Commercial The DTM (Dialogues Testing Method) tool uses a custom activity model (actions, decisions...), and selects tests based on structural coverage (multiple condition or all path).
fMBT 2014   Custom (AAL) Open source fMBT (free Model-Based Testing) generates test cases from models written in the AAL/Python pre/postcondition language using different heuristics (random, weighted random, lookahead...).
GraphWalker 2014   FSM Open source Test generation from Finite State Machines. Search algoritms: A* or random, with a limit for various coverage criteria (state, edge, requirement). Formerly called as mbt.
JSXM 2014 [DBI12] EFSM (Stream X-machines) Academic JSXM is model animation and test generation tool that uses a kind of EFSMs as its input. The generated tests can be transformed to JUnit test cases.
JTorX 2014 [B10] LTS Open source JTorX is a reimplementation of TorX in Java with additional features. The LTS specification can be given in multiple format, and it can interact on-the-fly with the implementation under test.
MaTeLo 2013 [DZ03] Markov chains Commercial 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.
MBTsuite 2016 UML or BPMN Commercial MBTsuite can generate test cases from UML models based on various coverage criteria (path, edge...) or randomly. It can import model from several model editors and it is integrated with various test management and test execution tools.
MISTA 2013 [D+14] PrT net Academic MISTA generates test cases from high-level Petri nets, and using a mapping it can generate executable test code for various platforms (JUnit, NUnit, Selenium...). It can be used for functional or security testing.
Modbat 2015 [A+15b] EFSM (Scala-based DSL) Open source Modbat is a model-based testing tool that is based on annotated (extended) finite-state machines. It is specialized to testing the APIs. Modbat provides a domain-specific modeling language with features for probabilistic and non-deterministic transitions, component models with inheritance, and exceptions.
ModelJUnit 2014 [U12] EFSM Open source ModelJUnit allows you to write simple finite state machine (FSM) models or extended finite state machine (EFSM) models as Java classes, then generate tests from those models and measure various model coverage metrics.
MoMuT::UML 2014 [A+15] UML state machines, OOAS Academic MoMuT is a family of automated, model-based test case generation tools that can work off UML State Machines, Assume-Guarantee Contracts (REQS), and Object Oriented Action Systems (OOAS). The tools feature a fault-based test case generation strategy (using mutation operators).
OSMO 2014 [KP12] model program in Java Open source OSMO uses model programs written and annotated in Java, and creates tests by exploring these models using different strategies (random, using constraints to guide...).
PyModel 2013 [J11] Python source Open source PyModel supports offline and on-the-fly testing. It uses composition for scenario control. Coverage can be guided by a programmable strategy.
RT-Tester 2014 [P13] UML/SysML, Matlab Commercial RT-Tester starts from UML/SysML or Matlab models, transforms them to a internal representation based on Kripke structures, transform requirements to LTL formulae, and generates test cases using an SMT solver based on the goals from requirements and various model coverage criteria.
Smartesting CertifyIt 2014 [BGLP08] UML + OCL Commercial 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.
Spec Explorer 2013 [V+08] model programs in C# Commercial Spec Explorer 2010 is the successor of the AsmL Test Tool and Spec Explorer 2004, and is now integrated into Visual Studio. The models can be written in C#, and test generation is directed with test purposes written in the Cord language.
Tcases 2015 Custom Open source Tcases is a combinatorial testing tool where the inputs of the system could be specified in an XML file (with conditions, failure values, don't cares, etc.). Tcases can generate n-wise or randomized test suites.
TEMPPO 2014 [BM08] Task flow model Commercial TEMPPO Designer (previosly IDATG) was initally developed to model GUIs, but it later was extened to API testing. It supports several external test execution framework. It was used by European Space Agency (ESA).
TestCast 2014 [EKRV06] UML State Machines Commercial TestCast MBT Edition generates TTCN-3 test cases from UML State Machines based on requirement and model structural coverage. The product is the successor of the MOTES prototype tool.
TestOptimal 2013   (E)FSM Commercial 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.
T-VEC 2013   Simulink Commercial T-VEC Tester for Simulink and Stateflow generates test cases for MatthWorks Simulink models based on various structural coverage criteria.

Tools not developed any more

AETG 2007 D+99 custom (AETGSpec textual notation) AETG is implemented as a web application to generate tests from requirements using pairwise coverage.
Cow_Suite 2003 [BBM02] UML Use Case and Sequence Diagrams Cow_Suite generates test cases from UML models according to structural coverage criteria.
GATeL 2004 [MB04] 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. (Tool web page not available any more.)
JUMBL 2010 [P03] Markov chains Academic Java Usage Model Builder Library (JUMBL) is a set of command-line and GUI tools supporting automated, model-based, statistical testing of systems.
NModel 2010 [JVCS07] model program written in C# Open source 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.
SAL-ATG 2011 [HMR05] custom (transition system) Open source Test generation using the SAL (Symbolic Analysis Laboratory) model checker at SRI International. Many optimization technique implemented which are useful for test generation, like bounded model checking.
SCOOTER 2005 [A+07] 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.
STG 2007 [DJRZ02] 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.
TGV 2004 JJ05 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 [TB03] 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 [PS08] 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. (Tool web page not available any more.)
UPPAAL Cover 2010 [H+08] timed automata Academic 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 [H+08] timed automata Academic UPAAL for Testing Realtime System ONline generates test suites on-the-fly with timing information for conformance testing.

MBT Case studies, projects and conferences

Case studies:

Case study Year Ref. Description
GSM 11-11 2004 [BLLP04] 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 [GKSB11] 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 [HN04] 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. See 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:


[A+15] B. Aichernig et al. (2015) "MoMuT::UML Model-based Mutation Testing for UML", In Proc. of ICST'15, IEEE, pp. ??
[A+15b] C. Artho, M. Seidl, Q. Gros, E.-H. Choi, T. Kitamura, A. Mori, R. Ramler, and Y. Yamagata (2015) "Model-Based Testing of Stateful APIs with Modbat," In Proc. of 30th IEEE/ACM International Conference on Automated Software Engineering (ASE 2015), pp. 858-863. DOI: 10.1109/ASE.2015.95
[A+07] S. Ali et al. (2007) "A state-based approach to integration testing based on UML models," Information and Software Technology, 49:11-12, pp. 1087-1106. DOI: 10.1016/j.infsof.2006.11.002
[B10] A. Belinfante (2012) "JTorX: a Tool for On-Line Model-Driven Test Derivation and Execution". In Proc. of TACAS'10, Springer, pp. 266-270. DOI: 10.1007/978-3-642-12002-2_21
[BBM02] F. Basanieri, A. Bertolino, E. Marchetti (2002) "The Cow_Suite Approach to Planning and Deriving Test Suites in UML Projects", In Proc. of UML'02, Springer, pp. 383-397. DOI: 10.1007/3-540-45800-X_30
[BGLP08] F. Bouquet, C. Grandpierre, B. Legeard, and F. Peureux (2008) "A test generation solution to automate software testing," In Proc. of Workshop on Automation of Software Test, ACM, pp. 45-48. DOI: 10.1145/1370042.1370052
[BLLP04] E. Bernard, B. Legeard, X. Luck, and F. Peureux (2004) "Generation of test sequences from formal specifications: GSM 11-11 standard case study," Software: Practice and Experience, 34:10, pp. 915-948. DOI: 10.1002/spe.597
[BM08] A. Beer, S. Mohacsi (2008) "Efficient Test Data Generation for Variables with Complex Dependencies", In Proc. of ICST'08, pp. 3-11. DOI: 10.1109/ICST.2008.10
[D+99] S. Dalal et al. (1999) "Model-based testing in practice," In Proc. of ICSE'99, pp. 285-294. DOI: 10.1109/ICSE.1999.841019
[D+14] D. Xu et al. (2014) "An Automated Test Generation Technique for Software Quality Assurance", IEEE Tran. on Reliability. DOI: 10.1109/TR.2014.2354172
[DBI12] D. Dranidis, K. Bratanis and F. Ipate (2012) "JSXM: a tool for automated test generation". In Proc. of SEFM'12. DOI: 10.1007/978-3-642-33826-7_25
[DJRZ02] D. Clarke, T. Jeron, V. Rusu, and E. Zinovieva (2002) "STG: A Symbolic Test Generation Tool," In Proc. TACAS'02, Springer, pp. 151-173. DOI: 10.1007/3-540-46002-0_34
[DZ03] W. Dulz and Fenhua Zhen (2003) "MaTeLo - statistical usage testing by annotated sequence diagrams, Markov chains and TTCN-3," In Proc. of Quality Software, pp. 336-342. DOI: 10.1109/QSIC.2003.1319119
[EKRV06] J. Ernits, A. Kull, K. Raiend, and J. Vain (2006) "Generating Tests from EFSM Models Using Guided Model Checking and Iterated Search Refinement," In Proc. of Formal Approaches to Software Testing and Runtime Verification, Springer, pp. 85-99. DOI: 10.1007/11940197_6
[FS14] M. Fowler, H.-J. Scherer (2104) "An adaptive software solution for generating test cases based on business process models," White paper, BPM-X GmbH
[GKSB11] Grieskamp, W., Kicillof, N., Stobie, K. and Braberman, V. (2011), "Model-based quality assurance of protocol documentation: tools and methodology." STVR, 21:1, pp. 55-71. DOI: 10.1002/stvr.427
[H07] A. Huima (2007) "Implementing Conformiq Qtronic," Testing of Software and Communicating Systems, Springer, pp. 1-12. DOI: 10.1007/978-3-540-73066-8_1
[H+08] A. Hessel et al. (2008) "Testing Real-Time Systems Using UPPAAL," In Proc of. Formal Methods and Testing, Springer, pp. 77-117. DOI: 10.1007/978-3-540-78917-8_3
[HLSC01] Hyoung Seok Hong, Insup Lee, Oleg Sokolsky, Sung Deok Cha (2001) Automatic Test Generation from Statecharts Using Model Checking, Technical Report MS-CIS-01-07, Link
[HMR05] G. Hamon, L. de Moura, and J. Rushby (2005) "Automated Test Generation with SAL", CSL Technical Note. URL
[HN04] A. Hartman and K. Nagin (2004) "The AGEDIS tools for model based testing," SIGSOFT Softw. Eng. Notes, 29:4, pp. 129-132. DOI: 10.1145/1013886.1007529
[J11] J. Jacky (2011), "PyModel: Model-based testing in Python", Proc. of the 9th Python in Science Conf. (SCIPY 2011) link.
[JJ05] C. Jard and T. Jeron (2005) "TGV: theory, principles and algorithms," STTT, 7:4, pp. 297-315. DOI: 10.1007/s10009-004-0153-x
[JVCS07] J. Jacky, M. Veanes, C. Campbell, and W. Schulte (2007) Model-Based Software Testing and Analysis with C#, Cambridge University Press, 2007.
[KP12] T. Kanstrén, O-P. Puolitaival (2012) "Using Built-In Domain-Specific Modeling Support to Guide Model-Based Test Generation", In Proc. of MBT'12. DOI: 10.4204/EPTCS.80.5
[MB04] B. Marre and B. Blanc (2004) "Test Selection Strategies for Lustre Descriptions in GATeL," In Proc. of MBT'04, pp. 93-111. DOI: 10.1016/j.entcs.2004.12.010.
[P03] S.J. Prowell (2003) "JUMBL: A Tool for Model-Based Statistical Testing," In Proc. of HICSS'03, IEEE. DOI: 10.1109/HICSS.2003.1174916
[P13] J. Peleska (2013) "Industrial-Strength Model-Based Testing - State of the Art and Current Challenges". In Proc. Eighth Workshop on Model-Based Testing, pp. 3-28 DOI: 10.4204/EPTCS.111.1
[PS08] S. Pietsch and B. Stanca-Kaposta (2008) "Model-based testing with UTP and TTCN-3 and its application to HL7," Technical report, Testing Technologies IST GmbH. URL
[TB03] J. Tretmans and H. Brinksma (2003) "TorX: Automated Model-Based Testing," In Proc. of European Conf. on Model-Driven Software Engineering, Nuremberg, Germany. pp. 31-43
[U12] M Utting (2012) "How to design extended finite state machine test models in Java." In: Model-Based Testing for Embedded Systems, chapter 6, pages 147-170. CRC Press.
[V+08] M. Veanes et al. (2008) "Model-Based Testing of Object-Oriented Reactive Systems with Spec Explorer," Formal Methods and Testing, Springer, pp. 39-76. DOI: 10.1007/978-3-540-78917-8_2
FTG Automatic Test Generation from Formal Specifications at NIST by Ammann and Black. Lot of useful papers, e.g. using mutation techniques and model checkers.
MBT model-based-testing.org - a site created by Harry Robinson. Not maintained any more, but there are a lot of links to publications.

Last modified: 2017. 09. 25.