White Box Testing
Test your code
   Home      Tools      ModelBasedTesting
Uppaal is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.).
Uppaal TRON is a testing tool, based onUppaal engine, suited for black-box conformance testing of timed systems, mainly targeted for embedded software commonly found in various controllers. By online we mean that tests are derived, executed and checked simultaneously while maintaining the connection to the system in real-time.

The TorX tool is a prototype testing tool for conformance testing of reactive software. The tool requires a real implementation and a (formal) specification of that implementation. The specification describes the system behaviour that the real implementation is allowed to perform. The TorX tool is the arbiter that checks the correct behaviour of a real implementation during its execution based on the formal specification. Note: it is also possible to use the simulation of a (formal) specification as ``implementation''.

The TorX tool is developed at theFormal Methods and Tools research group at the University of Twente (UT) in the Netherlands, in close collaboration withEindhoven University of Technology (TUE),Philips Research Laboratories and Lucent Technologies. The TorX tool is the product of theCôte de Resyste project, a project funded bythe Dutch Technology Foundation STW. Its main goal was the development of methods, techniques, and tools to support the automatic generation of tests from specifications, as well as their implementation, execution and analysis. This is accomplished in the academic prototype test tool TorX, one of the results produced by the project.

MISTA is a tool for model-based test generation and execution. It is suitable for function testing, acceptance testing, GUI testing, security testing, and programmer testing.

·       It uses lightweight high-level Petri nets as a visual modeling notation (a superset of finite state machines and extended finite state machines). Both control-oriented and data-oriented test models can be specified. Test models can be animated and verified. 

·    It provides test generators for comprehensive coverage criteria of test models, including reachability coverage, reachability with sneak paths, state coverage, transition coverage, depth coverage, goal coverage, random walk, counterexamples of model checking, deadlock/termination state coverage, and given sequences. Pairwise and partial order techniques are options for reducing the size of test suites.

·    It supports a number of languages (Java, C, C++, C#, HTML, and VB) and test frameworks (e.g., JUnit, NUnit, Selenium IDE, and Robot Framework) for offline test execution.

·    It supports on-the-fly testing and online execution of generated tests through Selenium WebDriver or a RPC protocol (JSON-RPC or XML-RPC).


The Java Usage Model Builder Library (JUMBL) is a set of command-line and GUI tools supporting automated, model-based, statistical testing of systems.

To find out more about this kind of testing and how the JUMBL supports it, click here.

JUMBL 5.0 is the current released version. More information is available here.

The JUMBL list is an email list for announcements related to development.

The JUMBL is available to selected formal and informal research partners. For information on obtaining the JUMBL
Critical systems Topcased is a software environment primarily dedicated to the realization of critical embedded systems including hardware and/or software.

Modeling Topcased promotes model-driven engineering and formal methods as key technologies.

Open-source Topcased is released as free/libre/open-source software by a group of partners from various organisations.
ModelJUnit is a Java library that extends JUnit to supportmodel-based testing. Models are extended finite state machines that are written in a familiar and expressive language: Java. ModelJUnit is an open source tool, released under the GNU GPL license.
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. The principles behind ModelJUnit are described in Sections 5.2 and 5.3 of our book, Practical Model-Based Testing. It is also possible to use ModelJUnit from within the Groovy language, assome Groovy person shows here.

The main features of GraphWalker are:

  • No UML

    GraphWalker's own ruleset in conjunction with GraphML, is easier to get started with than UML. As testers, we do not need all functionality that UML has to offer.
  • No exit/stop points

    The idea behind this, is that we want long, unpredictable test sequences. We do not want to walk the same path every time we execute a test. We want variation, spiced with randomness. This will create a better 'test coverage' of the system under test.
    The way to tell GraphWalker to stop generating test sequences are done by means of Stop Criterias, passed as arguments to the tool.
  • Online

    GraphWalker supports online test sequence generation. Using the online mode, the tool is capable of  testing non-deterministic systems. In essence, this means that the path walked through the model is decided runtime, during the actual test execution. This is very helpful if your test execution tool needs to communicate with the model during the test.
  • Jump between models

    GraphWalker supports switching models when traversing them. This enables re-usage of models and implemented code. See model switching article.
  • Event-driven

    GraphWalker will support (from version 2.5.1-SNAPSHOT) the possibility to switch model caused by an event. For example, let's say we have a model that executes the navigation of the GUI of a mobile phone. At any point in that execution, an incoming call will be such an event that will switch from navigating the GUI, to a model that handles the call.

JTorX is a tool to test whether the ioco testing relation holds between a given specification and a given implementation.
It can do so for Straces and Utraces of the specification.
The specification is given as Labelled Transition System (LTS) - represented for example in Aldebaran (.aut) or GraphML (.graphml) format,
or as Symbolic Transition System (STS).
The implementation is either also given as LTS, or it is given as a real program, in which case JTorX will need to be able to interact with it.
JTorX is out-of-the-box able to interact with programs that communicate on their standard input and output, or via tcp, using the same labels as in the specification.
For other programs an adapter has to be given.
JTorX is able to use adapter programs that have been developed for TorX.

JTorX is a reimplementation of the core functionality of TorX in Java -- with additional features added.

Compared to TorX, JTorX is based on more modern theory, and JTorX is much easier to deploy (regarding both installation and use).
JET is an automated unit testing tool for Java classes annotated with JML specifications; JML is a formal interface specification language for Java to document the behavior of Java classes and interfaces. JET tests each method of the class under test separately. For each method, it generates a collection of test data, executes them, and decides test results (i.e., pass/fail) by using JML specifications as test oracles, thereby fully automating unit testing of Java classes. [more from tutorial]

JET is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License.

Some of JET's features include:

  • Written in Java
  • Fully automated unit testing
  • Tests exported as JUnit test classes
  • Lightweight IDE for Java/JML
Spec Explorer
Spec Explorer is a tool that extends Visual Studio for modeling software behavior, analyzing that behavior by graphical visualization, model checking, and generating standalone test code from models. Behavior is modeled in two ways: by writing rules in C# (with dynamic data-defined state spaces) and by defining model scenarios as action patterns in a regular-expression style.
One of Spec Explorer’s major features is the ability to compose models written in these two styles. This technique enables users to slice out test cases from large state machines to achieve test purposes by defining relevant scenarios, thus tackling the notorious state-space explosion problem that is so pervasive in model-based testing. Spec Explorer also supports combinatorial interaction testing with a rich set of features.
NModel is a model-based testing and analysis framework for model programs written in C#. It is explained and used in the book Model-based Software Testing and Analysis with C#.

In contrast with conventional unit testing, where a test engineer must code each test case, model-based testing is recommended where so many test cases are needed that it would be infeasible to code them all by hand. It is especially indicated for testing behaviors with data- and history-dependence and non determinism, where many different variations (data values, interleavings etc.) should be tested for each scenario (or use case). Model-based testing has been applied to communication protocols, web applications, embedded control systems, and graphical user interfaces.

The NModel release includes:
The library also exposes the functionality of mpv, otg, ct and more, so you may write your own tools which are more closely adapted to your environment, or which provide other capabilities.


GUIs evolve rapidly and writing GUI test cases is notoriously labor-intensive.

With GUITAR, there is no need to manually handcraft GUI test cases, they are automatically generated.

GUITAR provides an end-to-end testing solution for GUI applications. The testing process consists of 4 main steps:

1. Ripping: Automatically expand hidden GUI elements (e.g., sub-menus, sub-windows) and capture the GUI structure using a crawler-like tool called GUI Ripper

2. Model construction: Construct a GUI model from the GUI structure (e.g., Event-flow Graph (EFG))

3. Test case generation: Generate test cases by walking on the model with graph traversal algorithms

4. Replaying: Execute test cases and verify the results

Some additional features:

  • Support for many different GUI widget toolkits
  • Transform the models into various formats such as GraphViz, UCINET, GEXF etc

IFx-OMEGA is a compiler / simulator / model-checker for a rich subset of UML 2.2 / SysML 1.1, based on the IF model checker from VERIMAG.

IFx-OMEGA originated in the European project IST OMEGA, and was further developed with support from other projects including IST ASSERT, ESA Activity 3-12639 and ESA FullMDE.

IFx-OMEGA may be used to validate and verify asynchronous timed system models with complex dynamics. It is based on a rigorous semantics, especially suited for critical real-time embedded systems.
ATS4 AppModel

ATS4 AppModel is an application flow design tool supporting application specification work, model based testing and test script generation. It provides simple interface to manage complex models. ATS4 AppModel is part of Nokia ATS tool family.

ATS 4 AppModel Main Features

  • Graphical representation of menu flow structure of phone / application
  • Advanced graph flow design and simulation tools
  • Automatic document (Test specification) generation from the model in multiple languages (e.g. Chinese, Hindi, Arabic)
  • Automatic test script generation from user and system event descriptions
  • Support for dynamic step by step test execution
  • Support for any external UI Design tool
  • Possibility to automatically import screen capture images directly from phone
  • Can be extended to use any keyword based test tool
Towards easier deployment of MBT in the domain of smartphone application GUI testing, Tampere University of Technology, Department of Software Systems has developed a prototype toolset, called TEMA, and a methodology for online test generation for smartphone GUI testing. The methodology is based on long-term research on MBT and practical case-studies with industrial partners. The features of TEMA’s two-tier modeling approach include the ability to reuse high-level models as the basis of test generation among different smartphone platforms. Moreover, we are able to test application interactions in long period test runs revealing robustness issues, which are typically out of reach of conventional test automation tools as well as off-line model-based tools that produce shorter test cases.
Cow_Suite provides an integrated and practical approach to the strategic generation and planning of UML-based test suites, since the early stages of system analysis and modeling.

It consists of two original components working in combination:
  • the Cowtest strategy, which organizes the testing process and helps the manager to select among the many potential test cases,
  • the UIT method, which performs the automated generation of test cases from the UML diagrams.
The approach can be used in incremental way, starting from the preliminary (even incomplete) UML diagrams, and is applied to integration subsystems, as interactively selected by the tester.

The emphasis is on usability, in that we use exactly the same UML diagrams developed for analysis and design, without requiring any additional formalism or ad-hoc effort specifically for testing purposes.

Cow_Suite has been implemented in a prototype tool, and is currently being validated in an industrial development environment.
For QA professionals and test engineers who are looking to innovate their testing process, TestOptimal is an integrated next-generation test design and test automation toolset powered by Model-Based Testing (MBT). Unlike QTP and TestComplete, TestOptimal helps you bring agility and efficiency to your testing process and shorten your testing cycle.

TestOptimal BasicMBT, ProMBT, Enterprise, RuntimeMBT and SvrMgr are a suite of model-based test automation tools for functional testing and load/performance testing. TestOptimal combines Model- Based Testing (MBT) and Data-Driven Testing (DDT) to provide you a powerful test case generation and test automation tool.

MBT enables you to find defects earlier in the development cycle and respond to changes quickly and efficiently. Animation of test execution enables you to gain insight and perform visual validation on the model. Track requirement coverage and visualize test cases in various graphs. Choose one of many algorithms to generate test sequences for desired test coverage. Re-purpose same models and automation scripts for load and performance testing. TestOptimal can help you reduce development cycle, achieve unprecedented test coverage and improve response to changes while gaining higher confidence in your software delivery.
PyModel includes an analyzer for validating models, visualizing their behavior, and checking their safety properties.

PyModel can generate offline tests which are similar to unit tests, but the typical way to use PyModel is on-the-fly testing, where the test runner uses the model to compute the test run as it executes, so test runs can be as long as needed. On-the-fly testing can cope with nondeterminism and asynchrony in the system under test.

PyModel can combine models using composition, guide tests through programmed scenarios, and focus test coverage according to programmed strategies.
It is model-based testing tool that helps to automatically generate TTCN-3 test scripts.
Modelling stateful systems
Validating models via animation
Automatically generating tests for testing the implementation
Transforming the tests to executable tests in the language of the implementation (e.g. JUnit)
Incremental testing of object-oriented applications
AETG Web Service
The AETGTM Web Service generates test cases from a model of your requirements. It uses combinatorial design techniques to find a minimal test-case set that covers all pairwise interactions among input values.

By using the AETG Web Service, you will be able to create robust and efficient test cases faster and more comprehensively than ever before. You will achieve:

  • High-quality test cases
  • Rapidly generated test plans
  • Reduced incidence of mission-critical software bugs.
This website is to help and support in white box testing technologies, tools and resources. Please Contact Us to publish your articles tutorial on http://www.whiteboxtest.com/