Skip to main content.


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 on Uppaal 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.

Below are a screenshot of smart-lamp controller Java applet demo and automatically generated signal flow diagram of the system model:

Java application mimicking a light controller Signal flow among processes in the smart lamp system model

Like Uppaal, Uppaal TRON is free for non-profit use, e.g. for evaluation, research, and teaching purposes. For more details please read the license.

Latest News

Version 1.5 released

17 June 2009

New preview release with fixes for usability issues. A new user-manual draft is available for building custom adapters. See Linux README and Windows README for details.